Theorem dfss4 3731

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

Assertion

Ref	Expression
dfss4

Proof of Theorem dfss4

Dummy variable is distinct from all other variables.

Step	Hyp	Ref	Expression
1		sseqin2 3716	. 2
2		eldif 3485	. . . . . . 7
3	2	notbii 296	. . . . . 6
4	3	anbi2i 694	. . . . 5
5		elin 3686	. . . . . 6
6		abai 795	. . . . . 6
7		iman 424	. . . . . . 7
8	7	anbi2i 694	. . . . . 6
9	5, 6, 8	3bitri 271	. . . . 5
10	4, 9	bitr4i 252	. . . 4
11	10	difeqri 3623	. . 3
12	11	eqeq1i 2464	. 2
13	1, 12	bitr4i 252	1

Syntax hints:  -.wn 3  ->wi 4  <->wb 184  /\wa 369  =wceq 1395  e.wcel 1818  \cdif 3472  i^icin 3474  C_wss 3475

This theorem is referenced by:  dfin4  3737  sorpsscmpl  6591  sbthlem3  7649  fin23lem7  8717  fin23lem11  8718  compsscnvlem  8771  compssiso  8775  isf34lem4  8778  efgmnvl  16732  frlmlbs  18831  isopn2  19533  iincld  19540  iuncld  19546  clsval2  19551  ntrval2  19552  ntrdif  19553  clsdif  19554  cmclsopn  19563  cmntrcld  19564  opncldf1  19585  indiscld  19592  mretopd  19593  restcld  19673  pnrmopn  19844  conndisj  19917  hausllycmp  19995  kqcldsat  20234  filufint  20421  cfinufil  20429  ufilen  20431  alexsublem  20544  bcth3  21770  inmbl  21952  iccmbl  21976  mbfimaicc  22040  i1fd  22088  itgss3  22221  frgrawopreg2  25051  iundifdifd  27429  iundifdif  27430  cldssbrsiga  28158  kur14lem4  28653  mblfinlem3  30053  mblfinlem4  30054  ismblfin  30055  itg2addnclem  30066  cldbnd  30144  clsun  30146  fdc  30238  lincext2  33056

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-dif 3478  df-in 3482  df-ss 3489