Metamath Proof Explorer

Theorem ssindif0

Description: Subclass expressed in terms of intersection with difference from the universal class. (Contributed by NM, 17-Sep-2003)

Ref Expression
Assertion ssindif0 
|- ( A C_ B <-> ( A i^i ( _V \ B ) ) = (/) )

Proof

Step Hyp Ref Expression
1 disj2 
 |-  ( ( A i^i ( _V \ B ) ) = (/) <-> A C_ ( _V \ ( _V \ B ) ) )
2 ddif 
 |-  ( _V \ ( _V \ B ) ) = B
3 2 sseq2i 
 |-  ( A C_ ( _V \ ( _V \ B ) ) <-> A C_ B )
4 1 3 bitr2i 
 |-  ( A C_ B <-> ( A i^i ( _V \ B ) ) = (/) )