Can anybody help me to understand the definition of Disjointness:
df-disj $a |- ( Disj_ x e. A B <-> A. y E* x e. A y e. B ) $.
? What means x, A, and B here?
What about my alternative definition as 1-ary predicate:
_disj_ A <-> A. B e. A A. C e. A ( B = C \/ B i^i C = (/) )
? Would it be provable:
$p _disj_ A <-> Disj_ x e. A B $= ? $.
?
Thank you for your help!
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion visit
https://groups.google.com/d/msgid/metamath/63763d29-b77a-4586-8664-74882baeaca6%40gmx.de.
