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 )