Metamath Proof Explorer


Theorem disj3

Description: Two ways of saying that two classes are disjoint. (Contributed by NM, 19-May-1998)

Ref Expression
Assertion disj3 AB=A=AB

Proof

Step Hyp Ref Expression
1 pm4.71 xA¬xBxAxA¬xB
2 eldif xABxA¬xB
3 2 bibi2i xAxABxAxA¬xB
4 1 3 bitr4i xA¬xBxAxAB
5 4 albii xxA¬xBxxAxAB
6 disj1 AB=xxA¬xB
7 dfcleq A=ABxxAxAB
8 5 6 7 3bitr4i AB=A=AB