This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- ( ( A i^i B ) = (/) <-> A = ( A \ B ) )

Proof

Step Hyp Ref Expression
1 pm4.71 
 |-  ( ( x e. A -> -. x e. B ) <-> ( x e. A <-> ( x e. A /\ -. x e. B ) ) )
2 eldif 
 |-  ( x e. ( A \ B ) <-> ( x e. A /\ -. x e. B ) )
3 2 bibi2i 
 |-  ( ( x e. A <-> x e. ( A \ B ) ) <-> ( x e. A <-> ( x e. A /\ -. x e. B ) ) )
4 1 3 bitr4i 
 |-  ( ( x e. A -> -. x e. B ) <-> ( x e. A <-> x e. ( A \ B ) ) )
5 4 albii 
 |-  ( A. x ( x e. A -> -. x e. B ) <-> A. x ( x e. A <-> x e. ( A \ B ) ) )
6 disj1 
 |-  ( ( A i^i B ) = (/) <-> A. x ( x e. A -> -. x e. B ) )
7 dfcleq 
 |-  ( A = ( A \ B ) <-> A. x ( x e. A <-> x e. ( A \ B ) ) )
8 5 6 7 3bitr4i 
 |-  ( ( A i^i B ) = (/) <-> A = ( A \ B ) )