Theorem dfss4 3707

Description: Subclass defined in terms of class difference. See comments under dfun2 3708. (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 3681	. 2 |- ( A C_ B <-> ( B i^i A ) = A )
2		eldif 3446	. . . . . . 7 |- ( x e. ( B \ A ) <-> ( x e. B /\ -. x e. A ) )
3	2	notbii 297	. . . . . 6 |- ( -. x e. ( B \ A ) <-> -. ( x e. B /\ -. x e. A ) )
4	3	anbi2i 698	. . . . 5 |- ( ( x e. B /\ -. x e. ( B \ A ) ) <-> ( x e. B /\ -. ( x e. B /\ -. x e. A ) ) )
5		elin 3649	. . . . . 6 |- ( x e. ( B i^i A ) <-> ( x e. B /\ x e. A ) )
6		abai 802	. . . . . 6 |- ( ( x e. B /\ x e. A ) <-> ( x e. B /\ ( x e. B -> x e. A ) ) )
7		iman 425	. . . . . . 7 |- ( ( x e. B -> x e. A ) <-> -. ( x e. B /\ -. x e. A ) )
8	7	anbi2i 698	. . . . . 6 |- ( ( x e. B /\ ( x e. B -> x e. A ) ) <-> ( x e. B /\ -. ( x e. B /\ -. x e. A ) ) )
9	5, 6, 8	3bitri 274	. . . . 5 |- ( x e. ( B i^i A ) <-> ( x e. B /\ -. ( x e. B /\ -. x e. A ) ) )
10	4, 9	bitr4i 255	. . . 4 |- ( ( x e. B /\ -. x e. ( B \ A ) ) <-> x e. ( B i^i A ) )
11	10	difeqri 3585	. . 3 |- ( B \ ( B \ A ) ) = ( B i^i A )
12	11	eqeq1i 2429	. 2 |- ( ( B \ ( B \ A ) ) = A <-> ( B i^i A ) = A )
13	1, 12	bitr4i 255	1 |- ( A C_ B <-> ( B \ ( B \ A ) ) = A )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 187   /\ wa 370   = wceq 1437   e. wcel 1872   \ cdif 3433   i^i cin 3435   C_ wss 3436

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401

This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-v 3082  df-dif 3439  df-in 3443  df-ss 3450

This theorem is referenced by:  dfin4  3713  sorpsscmpl  6596  sbthlem3  7693  fin23lem7  8753  fin23lem11  8754  compsscnvlem  8807  compssiso  8811  isf34lem4  8814  efgmnvl  17363  frlmlbs  19353  isopn2  20045  iincld  20052  iuncld  20058  clsval2  20063  ntrval2  20064  ntrdif  20065  clsdif  20066  cmclsopn  20075  cmntrcldOLD  20077  opncldf1  20098  indiscld  20105  mretopd  20106  restcld  20186  pnrmopn  20357  conndisj  20429  hausllycmp  20507  kqcldsat  20746  filufint  20933  cfinufil  20941  ufilen  20943  alexsublem  21057  bcth3  22297  inmbl  22493  iccmbl  22517  mbfimaicc  22587  i1fd  22637  itgss3  22770  frgrawopreg2  25777  difuncomp  28168  iundifdifd  28179  iundifdif  28180  cldssbrsiga  29017  unelcarsg  29152  kur14lem4  29940  cldbnd  30987  clsun  30989  mblfinlem3  31943  mblfinlem4  31944  ismblfin  31945  itg2addnclem  31957  fdc  32038  salincl  38105  lincext2  39869