Metamath Proof Explorer

Theorem disj1

Description: Two ways of saying that two classes are disjoint (have no members in common). (Contributed by NM, 19-Aug-1993)

Ref Expression
Assertion disj1 A B = x x A ¬ x B


Step Hyp Ref Expression
1 disj A B = x A ¬ x B
2 df-ral x A ¬ x B x x A ¬ x B
3 1 2 bitri A B = x x A ¬ x B