Theorem dfss4 3737

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

Assertion

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

Proof of Theorem dfss4

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		sseqin2 3722	. 2 |- ( A C_ B <-> ( B i^i A ) = A )
2		eldif 3491	. . . . . . 7 |- ( x e. ( B \ A ) <-> ( x e. B /\ -. x e. A ) )
3	2	notbii 296	. . . . . 6 |- ( -. x e. ( B \ A ) <-> -. ( x e. B /\ -. x e. A ) )
4	3	anbi2i 694	. . . . 5 |- ( ( x e. B /\ -. x e. ( B \ A ) ) <-> ( x e. B /\ -. ( x e. B /\ -. x e. A ) ) )
5		elin 3692	. . . . . 6 |- ( x e. ( B i^i A ) <-> ( x e. B /\ x e. A ) )
6		abai 793	. . . . . 6 |- ( ( x e. B /\ x e. A ) <-> ( x e. B /\ ( x e. B -> x e. A ) ) )
7		iman 424	. . . . . . 7 |- ( ( x e. B -> x e. A ) <-> -. ( x e. B /\ -. x e. A ) )
8	7	anbi2i 694	. . . . . 6 |- ( ( x e. B /\ ( x e. B -> x e. A ) ) <-> ( x e. B /\ -. ( x e. B /\ -. x e. A ) ) )
9	5, 6, 8	3bitri 271	. . . . 5 |- ( x e. ( B i^i A ) <-> ( x e. B /\ -. ( x e. B /\ -. x e. A ) ) )
10	4, 9	bitr4i 252	. . . 4 |- ( ( x e. B /\ -. x e. ( B \ A ) ) <-> x e. ( B i^i A ) )
11	10	difeqri 3629	. . 3 |- ( B \ ( B \ A ) ) = ( B i^i A )
12	11	eqeq1i 2474	. 2 |- ( ( B \ ( B \ A ) ) = A <-> ( B i^i A ) = A )
13	1, 12	bitr4i 252	1 |- ( A C_ B <-> ( B \ ( B \ A ) ) = A )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 184   /\ wa 369   = wceq 1379   e. wcel 1767   \ cdif 3478   i^i cin 3480   C_ wss 3481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3120  df-dif 3484  df-in 3488  df-ss 3495

This theorem is referenced by:  dfin4  3743  sorpsscmpl  6586  sbthlem3  7641  fin23lem7  8708  fin23lem11  8709  compsscnvlem  8762  compssiso  8766  isf34lem4  8769  efgmnvl  16605  frlmlbs  18700  isopn2  19401  iincld  19408  iuncld  19414  clsval2  19419  ntrval2  19420  ntrdif  19421  clsdif  19422  cmclsopn  19431  cmntrcld  19432  opncldf1  19453  indiscld  19460  mretopd  19461  restcld  19541  pnrmopn  19712  conndisj  19785  hausllycmp  19863  kqcldsat  20102  filufint  20289  cfinufil  20297  ufilen  20299  alexsublem  20412  bcth3  21638  inmbl  21820  iccmbl  21844  mbfimaicc  21908  i1fd  21956  itgss3  22089  frgrawopreg2  24866  iundifdifd  27243  iundifdif  27244  cldssbrsiga  27974  kur14lem4  28469  mblfinlem3  29971  mblfinlem4  29972  ismblfin  29973  itg2addnclem  29984  cldbnd  30062  clsun  30064  fdc  30156  lincext2  32493