Theorem dfss4 3693

Description: Subclass defined in terms of class difference. See comments under dfun2 3694. (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 3678	. 2 |- ( A C_ B <-> ( B i^i A ) = A )
2		eldif 3447	. . . . . . 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 3648	. . . . . 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 3585	. . 3 |- ( B \ ( B \ A ) ) = ( B i^i A )
12	11	eqeq1i 2461	. 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 1370   e. wcel 1758   \ cdif 3434   i^i cin 3436   C_ wss 3437

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3080  df-dif 3440  df-in 3444  df-ss 3451

This theorem is referenced by:  dfin4  3699  sorpsscmpl  6482  sbthlem3  7534  fin23lem7  8597  fin23lem11  8598  compsscnvlem  8651  compssiso  8655  isf34lem4  8658  efgmnvl  16333  frlmlbs  18351  isopn2  18769  iincld  18776  iuncld  18782  clsval2  18787  ntrval2  18788  ntrdif  18789  clsdif  18790  cmclsopn  18799  cmntrcld  18800  opncldf1  18821  indiscld  18828  mretopd  18829  restcld  18909  pnrmopn  19080  conndisj  19153  hausllycmp  19231  kqcldsat  19439  filufint  19626  cfinufil  19634  ufilen  19636  alexsublem  19749  bcth3  20975  inmbl  21157  iccmbl  21181  mbfimaicc  21245  i1fd  21293  itgss3  21426  iundifdifd  26064  iundifdif  26065  cldssbrsiga  26747  kur14lem4  27242  mblfinlem3  28579  mblfinlem4  28580  ismblfin  28581  itg2addnclem  28592  cldbnd  28670  clsun  28672  fdc  28790  frgrawopreg2  30793  lincext2  31122