Theorem dfss1 3637

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

Assertion

Ref	Expression
dfss1

Proof of Theorem dfss1

Step	Hyp	Ref	Expression
1		df-ss 3424	. 2
2		incom 3625	. . 3
3	2	eqeq1i 2456	. 2
4	1, 3	bitri 249	1

Syntax hints:  <->wb 184  =wceq 1370  i^icin 3409  C_wss 3410

This theorem is referenced by:  dfss5  3638  sseqin2  3651  onfr  4840  xpimasnOLD  5366  fndmdif  5890  sorpssin  6452  infxpenlem  8265  acndom2  8309  isf34lem5  8632  fpwwe2  8895  leiso  12298  isercolllem3  13230  incexc  13386  bitsinv1  13724  bitsinvp1  13731  bitsshft  13757  ressabs  14322  psssdm  15472  dprdsn  16622  ablfac1eu  16663  ablfaclem3  16677  ocv1  18197  resttopon  18865  restabs  18869  restopnb  18879  restperf  18888  ordtbas  18896  ordtrest2lem  18907  ordtrest2  18908  leordtvallem1  18914  leordtvallem2  18915  cnclsi  18976  ordtt1  19083  connsub  19125  cnconn  19126  nconsubb  19127  consubclo  19128  1stcfb  19149  kgentopon  19211  ptbasfi  19254  ptclsg  19288  dfac14lem  19290  xkoccn  19292  txcnmpt  19297  txtube  19313  xkoptsub  19327  xkopt  19328  kqsat  19404  kqcldsat  19406  ordthmeolem  19474  trfil1  19559  trfil2  19560  trufil  19583  divstgphaus  19793  trust  19904  metustfbasOLD  20240  metustfbas  20241  cfilucfilOLD  20244  cfilucfil  20245  xrsmopn  20489  lebnumii  20638  iscmet3  20904  resscdrg  20970  uniioombllem4  21166  mbflimsup  21244  lhop1  21586  lhop2  21587  wilthlem2  22507  ex-in  23751  fimacnvinrn2  26071  xppreima  26082  gtiso  26114  resf1o  26148  prsss  26464  ordtrestNEW  26469  ordtrest2NEWlem  26470  ordtrest2NEW  26471  probdsb  26923  totprobd  26927  cndprobtot  26937  ballotlemfmpn  26995  signsplypnf  27069  signsply0  27070  omsinds  27798  mblfinlem3  28552  mblfinlem4  28553  itg2addnclem2  28566  neibastop3  28705  sstotbnd2  28795  stoweidlem50  29967  lcvexchlem4  32963  lclkrlem2r  35450  mapdunirnN  35576

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 1709  ax-7 1729  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2429

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1702  df-clab 2436  df-cleq 2442  df-clel 2445  df-nfc 2598  df-v 3054  df-in 3417  df-ss 3424