Theorem disj4

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

	Ref	Expression
Assertion	disj4	⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ ↔ ¬ ( 𝐴 ∖ 𝐵 ) ⊊ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		disj3	⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ ↔ 𝐴 = ( 𝐴 ∖ 𝐵 ) )
2		eqcom	⊢ ( 𝐴 = ( 𝐴 ∖ 𝐵 ) ↔ ( 𝐴 ∖ 𝐵 ) = 𝐴 )
3		difss	⊢ ( 𝐴 ∖ 𝐵 ) ⊆ 𝐴
4		dfpss2	⊢ ( ( 𝐴 ∖ 𝐵 ) ⊊ 𝐴 ↔ ( ( 𝐴 ∖ 𝐵 ) ⊆ 𝐴 ∧ ¬ ( 𝐴 ∖ 𝐵 ) = 𝐴 ) )
5	3 4	mpbiran	⊢ ( ( 𝐴 ∖ 𝐵 ) ⊊ 𝐴 ↔ ¬ ( 𝐴 ∖ 𝐵 ) = 𝐴 )
6	5	con2bii	⊢ ( ( 𝐴 ∖ 𝐵 ) = 𝐴 ↔ ¬ ( 𝐴 ∖ 𝐵 ) ⊊ 𝐴 )
7	1 2 6	3bitri	⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ ↔ ¬ ( 𝐴 ∖ 𝐵 ) ⊊ 𝐴 )