Theorem dfss4 3739

Description: Subclass defined in terms of class difference. See comments under dfun2 3740. (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 3713	. 2 |- ( A C_ B <-> ( B i^i A ) = A )
2		eldif 3481	. . . . . . 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 3683	. . . . . 6 |- ( x e. ( B i^i A ) <-> ( x e. B /\ x e. A ) )
6		abai 795	. . . . . 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 3620	. . 3 |- ( B \ ( B \ A ) ) = ( B i^i A )
12	11	eqeq1i 2464	. 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 1395   e. wcel 1819   \ cdif 3468   i^i cin 3470   C_ wss 3471

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-dif 3474  df-in 3478  df-ss 3485

This theorem is referenced by:  dfin4  3745  sorpsscmpl  6590  sbthlem3  7648  fin23lem7  8713  fin23lem11  8714  compsscnvlem  8767  compssiso  8771  isf34lem4  8774  efgmnvl  16859  frlmlbs  18958  isopn2  19660  iincld  19667  iuncld  19673  clsval2  19678  ntrval2  19679  ntrdif  19680  clsdif  19681  cmclsopn  19690  cmntrcld  19691  opncldf1  19712  indiscld  19719  mretopd  19720  restcld  19800  pnrmopn  19971  conndisj  20043  hausllycmp  20121  kqcldsat  20360  filufint  20547  cfinufil  20555  ufilen  20557  alexsublem  20670  bcth3  21896  inmbl  22078  iccmbl  22102  mbfimaicc  22166  i1fd  22214  itgss3  22347  frgrawopreg2  25178  iundifdifd  27568  iundifdif  27569  cldssbrsiga  28331  unelcarsg  28455  kur14lem4  28850  mblfinlem3  30258  mblfinlem4  30259  ismblfin  30260  itg2addnclem  30271  cldbnd  30349  clsun  30351  fdc  30443  lincext2  33200