This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dfss4

Description: Subclass defined in terms of class difference. See comments under dfun2 . (Contributed by NM, 22-Mar-1998) (Proof shortened by Andrew Salmon, 26-Jun-2011)

Ref Expression
Assertion dfss4 
|- ( A C_ B <-> ( B \ ( B \ A ) ) = A )

Proof

Step Hyp Ref Expression
1 sseqin2 
 |-  ( A C_ B <-> ( B i^i A ) = A )
2 eldif 
 |-  ( x e. ( B \ A ) <-> ( x e. B /\ -. x e. A ) )
3 2 notbii 
 |-  ( -. x e. ( B \ A ) <-> -. ( x e. B /\ -. x e. A ) )
4 3 anbi2i 
 |-  ( ( x e. B /\ -. x e. ( B \ A ) ) <-> ( x e. B /\ -. ( x e. B /\ -. x e. A ) ) )
5 elin 
 |-  ( x e. ( B i^i A ) <-> ( x e. B /\ x e. A ) )
6 abai 
 |-  ( ( x e. B /\ x e. A ) <-> ( x e. B /\ ( x e. B -> x e. A ) ) )
7 iman 
 |-  ( ( x e. B -> x e. A ) <-> -. ( x e. B /\ -. x e. A ) )
8 7 anbi2i 
 |-  ( ( x e. B /\ ( x e. B -> x e. A ) ) <-> ( x e. B /\ -. ( x e. B /\ -. x e. A ) ) )
9 5 6 8 3bitri 
 |-  ( x e. ( B i^i A ) <-> ( x e. B /\ -. ( x e. B /\ -. x e. A ) ) )
10 4 9 bitr4i 
 |-  ( ( x e. B /\ -. x e. ( B \ A ) ) <-> x e. ( B i^i A ) )
11 10 difeqri 
 |-  ( B \ ( B \ A ) ) = ( B i^i A )
12 11 eqeq1i 
 |-  ( ( B \ ( B \ A ) ) = A <-> ( B i^i A ) = A )
13 1 12 bitr4i 
 |-  ( A C_ B <-> ( B \ ( B \ A ) ) = A )