Theorem dfss4 3645

Description: Subclass defined in terms of class difference. See comments under dfun2 3646. (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 3619	. 2 |- ( A C_ B <-> ( B i^i A ) = A )
2		eldif 3382	. . . . . . 7 |- ( x e. ( B \ A ) <-> ( x e. B /\ -. x e. A ) )
3	2	notbii 302	. . . . . 6 |- ( -. x e. ( B \ A ) <-> -. ( x e. B /\ -. x e. A ) )
4	3	anbi2i 705	. . . . 5 |- ( ( x e. B /\ -. x e. ( B \ A ) ) <-> ( x e. B /\ -. ( x e. B /\ -. x e. A ) ) )
5		elin 3585	. . . . . 6 |- ( x e. ( B i^i A ) <-> ( x e. B /\ x e. A ) )
6		abai 809	. . . . . 6 |- ( ( x e. B /\ x e. A ) <-> ( x e. B /\ ( x e. B -> x e. A ) ) )
7		iman 430	. . . . . . 7 |- ( ( x e. B -> x e. A ) <-> -. ( x e. B /\ -. x e. A ) )
8	7	anbi2i 705	. . . . . 6 |- ( ( x e. B /\ ( x e. B -> x e. A ) ) <-> ( x e. B /\ -. ( x e. B /\ -. x e. A ) ) )
9	5, 6, 8	3bitri 279	. . . . 5 |- ( x e. ( B i^i A ) <-> ( x e. B /\ -. ( x e. B /\ -. x e. A ) ) )
10	4, 9	bitr4i 260	. . . 4 |- ( ( x e. B /\ -. x e. ( B \ A ) ) <-> x e. ( B i^i A ) )
11	10	difeqri 3521	. . 3 |- ( B \ ( B \ A ) ) = ( B i^i A )
12	11	eqeq1i 2457	. 2 |- ( ( B \ ( B \ A ) ) = A <-> ( B i^i A ) = A )
13	1, 12	bitr4i 260	1 |- ( A C_ B <-> ( B \ ( B \ A ) ) = A )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 189   /\ wa 375   = wceq 1448   e. wcel 1891   \ cdif 3369   i^i cin 3371   C_ wss 3372

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1673  ax-4 1686  ax-5 1762  ax-6 1809  ax-7 1855  ax-10 1919  ax-11 1924  ax-12 1937  ax-13 2092  ax-ext 2432

This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1451  df-ex 1668  df-nf 1672  df-sb 1802  df-clab 2439  df-cleq 2445  df-clel 2448  df-nfc 2582  df-v 3015  df-dif 3375  df-in 3379  df-ss 3386

This theorem is referenced by:  dfin4  3651  sorpsscmpl  6570  sbthlem3  7671  fin23lem7  8733  fin23lem11  8734  compsscnvlem  8787  compssiso  8791  isf34lem4  8794  efgmnvl  17375  frlmlbs  19366  isopn2  20058  iincld  20065  iuncld  20071  clsval2  20076  ntrval2  20077  ntrdif  20078  clsdif  20079  cmclsopn  20088  cmntrcldOLD  20090  opncldf1  20111  indiscld  20118  mretopd  20119  restcld  20199  pnrmopn  20370  conndisj  20442  hausllycmp  20520  kqcldsat  20759  filufint  20946  cfinufil  20954  ufilen  20956  alexsublem  21070  bcth3  22310  inmbl  22507  iccmbl  22531  mbfimaicc  22601  i1fd  22651  itgss3  22784  frgrawopreg2  25791  difuncomp  28177  iundifdifd  28187  iundifdif  28188  cldssbrsiga  29016  unelcarsg  29150  kur14lem4  29938  cldbnd  30988  clsun  30990  mblfinlem3  31981  mblfinlem4  31982  ismblfin  31983  itg2addnclem  31995  fdc  32076  salincl  38241  salexct  38250  ovnsubadd2lem  38530  lincext2  40573