Metamath Proof Explorer

Theorem disjr

Description: Two ways of saying that two classes are disjoint. (Contributed by Jeff Madsen, 19-Jun-2011)

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

Proof

Step Hyp Ref Expression
1 ineqcom 
 |-  ( ( A i^i B ) = (/) <-> ( B i^i A ) = (/) )
2 disj 
 |-  ( ( B i^i A ) = (/) <-> A. x e. B -. x e. A )
3 1 2 bitri 
 |-  ( ( A i^i B ) = (/) <-> A. x e. B -. x e. A )