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 ABAA=

Proof

Step Hyp Ref Expression
1 inidm AA=A
2 ssdifin0 ABAAA=
3 1 2 eqtr3id ABAA=
4 0ss B
5 id A=A=
6 difeq2 A=BA=B
7 5 6 sseq12d A=ABAB
8 4 7 mpbiri A=ABA
9 3 8 impbii ABAA=