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

Metamath Proof Explorer

Theorem disj

Description: Two ways of saying that two classes are disjoint (have no members in common). (Contributed by NM, 17-Feb-2004) Avoid ax-10 , ax-11 , ax-12 . (Revised by GG, 28-Jun-2024)

Ref Expression
Assertion disj 
|- ( ( A i^i B ) = (/) <-> A. x e. A -. x e. B )

Proof

Step Hyp Ref Expression
1 df-in 
 |-  ( A i^i B ) = { y | ( y e. A /\ y e. B ) }
2 1 eqeq1i 
 |-  ( ( A i^i B ) = (/) <-> { y | ( y e. A /\ y e. B ) } = (/) )
3 eleq1w 
 |-  ( y = x -> ( y e. A <-> x e. A ) )
4 eleq1w 
 |-  ( y = x -> ( y e. B <-> x e. B ) )
5 3 4 anbi12d 
 |-  ( y = x -> ( ( y e. A /\ y e. B ) <-> ( x e. A /\ x e. B ) ) )
6 5 eqabcbw 
 |-  ( { y | ( y e. A /\ y e. B ) } = (/) <-> A. x ( ( x e. A /\ x e. B ) <-> x e. (/) ) )
7 imnan 
 |-  ( ( x e. A -> -. x e. B ) <-> -. ( x e. A /\ x e. B ) )
8 noel 
 |-  -. x e. (/)
9 8 nbn 
 |-  ( -. ( x e. A /\ x e. B ) <-> ( ( x e. A /\ x e. B ) <-> x e. (/) ) )
10 7 9 bitr2i 
 |-  ( ( ( x e. A /\ x e. B ) <-> x e. (/) ) <-> ( x e. A -> -. x e. B ) )
11 10 albii 
 |-  ( A. x ( ( x e. A /\ x e. B ) <-> x e. (/) ) <-> A. x ( x e. A -> -. x e. B ) )
12 2 6 11 3bitri 
 |-  ( ( A i^i B ) = (/) <-> A. x ( x e. A -> -. x e. B ) )
13 df-ral 
 |-  ( A. x e. A -. x e. B <-> A. x ( x e. A -> -. x e. B ) )
14 12 13 bitr4i 
 |-  ( ( A i^i B ) = (/) <-> A. x e. A -. x e. B )