Theorem disj4

Description: Two ways of saying that two classes are disjoint. (Contributed by NM, 21-Mar-2004)

	Ref	Expression
Assertion	disj4	|- ( ( A i^i B ) = (/) <-> -. ( A \ B ) C. A )

Proof

Step	Hyp	Ref	Expression
1		disj3	|- ( ( A i^i B ) = (/) <-> A = ( A \ B ) )
2		eqcom	|- ( A = ( A \ B ) <-> ( A \ B ) = A )
3		difss	|- ( A \ B ) C_ A
4		dfpss2	|- ( ( A \ B ) C. A <-> ( ( A \ B ) C_ A /\ -. ( A \ B ) = A ) )
5	3 4	mpbiran	|- ( ( A \ B ) C. A <-> -. ( A \ B ) = A )
6	5	con2bii	|- ( ( A \ B ) = A <-> -. ( A \ B ) C. A )
7	1 2 6	3bitri	|- ( ( A i^i B ) = (/) <-> -. ( A \ B ) C. A )