Metamath Proof Explorer


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 ( 𝐴 ⊆ ( 𝐵𝐴 ) ↔ 𝐴 = ∅ )