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 
|- ( A C_ ( B \ A ) <-> A = (/) )

Proof

Step Hyp Ref Expression
1 inidm 
 |-  ( A i^i A ) = A
2 ssdifin0 
 |-  ( A C_ ( B \ A ) -> ( A i^i A ) = (/) )
3 1 2 eqtr3id 
 |-  ( A C_ ( B \ A ) -> A = (/) )
4 0ss 
 |-  (/) C_ ( B \ (/) )
5 id 
 |-  ( A = (/) -> A = (/) )
6 difeq2 
 |-  ( A = (/) -> ( B \ A ) = ( B \ (/) ) )
7 5 6 sseq12d 
 |-  ( A = (/) -> ( A C_ ( B \ A ) <-> (/) C_ ( B \ (/) ) ) )
8 4 7 mpbiri 
 |-  ( A = (/) -> A C_ ( B \ A ) )
9 3 8 impbii 
 |-  ( A C_ ( B \ A ) <-> A = (/) )