Theorem ssdifeq0

Description: A class is a subclass of itself subtracted from another iff it is the empty set. (Contributed by Steve Rodriguez, 20-Nov-2015)

	Ref	Expression
Assertion	ssdifeq0	⊢ ( 𝐴 ⊆ ( 𝐵 ∖ 𝐴 ) ↔ 𝐴 = ∅ )

Proof

Step	Hyp	Ref	Expression
1		inidm	⊢ ( 𝐴 ∩ 𝐴 ) = 𝐴
2		ssdifin0	⊢ ( 𝐴 ⊆ ( 𝐵 ∖ 𝐴 ) → ( 𝐴 ∩ 𝐴 ) = ∅ )
3	1 2	eqtr3id	⊢ ( 𝐴 ⊆ ( 𝐵 ∖ 𝐴 ) → 𝐴 = ∅ )
4		0ss	⊢ ∅ ⊆ ( 𝐵 ∖ ∅ )
5		id	⊢ ( 𝐴 = ∅ → 𝐴 = ∅ )
6		difeq2	⊢ ( 𝐴 = ∅ → ( 𝐵 ∖ 𝐴 ) = ( 𝐵 ∖ ∅ ) )
7	5 6	sseq12d	⊢ ( 𝐴 = ∅ → ( 𝐴 ⊆ ( 𝐵 ∖ 𝐴 ) ↔ ∅ ⊆ ( 𝐵 ∖ ∅ ) ) )
8	4 7	mpbiri	⊢ ( 𝐴 = ∅ → 𝐴 ⊆ ( 𝐵 ∖ 𝐴 ) )
9	3 8	impbii	⊢ ( 𝐴 ⊆ ( 𝐵 ∖ 𝐴 ) ↔ 𝐴 = ∅ )