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		incom	|- ( A i^i B ) = ( B i^i A )
2	1	eqeq1i	|- ( ( A i^i B ) = (/) <-> ( B i^i A ) = (/) )
3		disj	|- ( ( B i^i A ) = (/) <-> A. x e. B -. x e. A )
4	2 3	bitri	|- ( ( A i^i B ) = (/) <-> A. x e. B -. x e. A )