Theorem dfss1 3702

Description: A frequently-used variant of subclass definition df-ss 3489. (Contributed by NM, 10-Jan-2015.)

Assertion

Ref	Expression
dfss1

Proof of Theorem dfss1

Step	Hyp	Ref	Expression
1		df-ss 3489	. 2
2		incom 3690	. . 3
3	2	eqeq1i 2464	. 2
4	1, 3	bitri 249	1

Syntax hints:  <->wb 184  =wceq 1395  i^icin 3474  C_wss 3475

This theorem is referenced by:  dfss5  3703  sseqin2  3716  onfr  4922  xpimasnOLD  5458  fndmdif  5991  fveqressseq  6027  sorpssin  6588  infxpenlem  8412  acndom2  8456  isf34lem5  8779  fpwwe2  9042  leiso  12508  isercolllem3  13489  incexc  13649  bitsinv1  14092  bitsinvp1  14099  bitsshft  14125  ressabs  14695  psssdm  15846  dprdsn  17083  ablfac1eu  17124  ablfaclem3  17138  ocv1  18710  resttopon  19662  restabs  19666  restopnb  19676  restperf  19685  ordtbas  19693  ordtrest2lem  19704  ordtrest2  19705  leordtvallem1  19711  leordtvallem2  19712  cnclsi  19773  ordtt1  19880  connsub  19922  cnconn  19923  nconsubb  19924  consubclo  19925  1stcfb  19946  kgentopon  20039  ptbasfi  20082  ptclsg  20116  dfac14lem  20118  xkoccn  20120  txcnmpt  20125  txtube  20141  xkoptsub  20155  xkopt  20156  kqsat  20232  kqcldsat  20234  ordthmeolem  20302  trfil1  20387  trfil2  20388  trufil  20411  qustgphaus  20621  trust  20732  metustfbasOLD  21068  metustfbas  21069  cfilucfilOLD  21072  cfilucfil  21073  xrsmopn  21317  lebnumii  21466  iscmet3  21732  resscdrg  21798  uniioombllem4  21995  mbflimsup  22073  lhop1  22415  lhop2  22416  wilthlem2  23343  ex-in  25146  fimacnvinrn2  27476  xppreima  27487  gtiso  27519  resf1o  27553  prsss  27898  ordtrestNEW  27903  ordtrest2NEWlem  27904  ordtrest2NEW  27905  probdsb  28361  totprobd  28365  cndprobtot  28375  ballotlemfmpn  28433  signsplypnf  28507  signsply0  28508  omsinds  29299  mblfinlem3  30053  mblfinlem4  30054  itg2addnclem2  30067  neibastop3  30180  sstotbnd2  30270  stoweidlem50  31832  lcvexchlem4  34762  lclkrlem2r  37251  mapdunirnN  37377  wnefimgd  37974

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-in 3482  df-ss 3489