Theorem dfss3 3493

Description: Alternate definition of subclass relationship. (Contributed by NM, 14-Oct-1999.)

Assertion

Ref	Expression
dfss3

Distinct variable groups:   ,   ,

Proof of Theorem dfss3

Step	Hyp	Ref	Expression
1		dfss2 3492	. 2
2		df-ral 2812	. 2
3	1, 2	bitr4i 252	1

Syntax hints:  ->wi 4  <->wb 184  A.wal 1393  e.wcel 1818  A.wral 2807  C_wss 3475

This theorem is referenced by:  ssrab  3577  elpwunsn  4070  eqsn  4191  uni0b  4274  uni0c  4275  ssint  4302  ssiinf  4379  sspwuni  4416  dftr3  4549  wefrc  4878  ordunisssuc  4985  rninxp  5451  fnres  5702  eqfnfv3  5983  funimass3  6003  ffvresb  6062  tfis  6689  smogt  7057  unifi  7829  unifi2  7830  fissuni  7845  fipreima  7846  cantnf  8133  cantnfOLD  8155  tz9.12lem3  8228  r1elss  8245  rankval3b  8265  rankonidlem  8267  bndrank  8280  iscard  8377  cfub  8650  cflm  8651  fin1a2s  8815  dcomex  8848  ttukeylem6  8915  unirnfdomd  8963  alephreg  8978  tskord  9179  gruuni  9199  intgru  9213  grudomon  9216  axgroth3  9230  suplem1pr  9451  supexpr  9453  supsr  9510  hashfun  12495  4sqlem19  14481  imasaddfnlem  14925  imasvscafn  14934  setcepi  15415  acsfiindd  15807  sylow2blem3  16642  sylow3lem6  16652  efgval2  16742  iscyggen2  16884  iscyg3  16889  issubdrg  17454  isdomn2  17948  ishil2  18750  rintopn  19418  isbasis2g  19449  tgval2  19457  eltg2b  19460  tgss2  19489  basgen2  19491  bastop1  19495  intcld  19541  unicld  19547  isclo  19588  isclo2  19589  neips  19614  opnnei  19621  neiptopnei  19633  isperf3  19654  ssidcn  19756  ist1-3  19850  cmpcov2  19890  cmpsub  19900  2ndcdisj2  19958  txkgen  20153  xkoinjcn  20188  tgqtop  20213  flimopn  20476  flfnei  20492  tmdcn2  20588  qustgplem  20619  cfil3i  21708  cmetcaulem  21727  ovolfioo  21879  ovolficc  21880  ovolicc2lem4  21931  opnmblALT  22012  xrlimcnp  23298  ubthlem1  25786  hasheuni  28091  dmvlsiga  28129  eulerpartlemr  28313  eulerpartlemn  28320  cvmlift2lem1  28747  cvmlift2lem12  28759  mclsax  28929  setinds  29210  tfisg  29284  wfisg  29289  frinsg  29325  fin2so  30040  isfne4  30158  isfne2  30160  isfne3  30161  neibastop2lem  30178  filnetlem4  30199  nninfnub  30244  unichnidl  30428  ispridl2  30435  isnacs2  30638  setindtrs  30967  dford3lem2  30969  dford3  30970  limciccioolb  31627  limcicciooub  31643  limcresiooub  31648  icccncfext  31690  stoweidlem31  31813  stoweidlem39  31821  fourierdlem8  31897  fourierdlem27  31916  fourierdlem38  31927  fourierdlem40  31929  fourierdlem41  31930  fourierdlem46  31935  fourierdlem48  31937  fourierdlem49  31938  fourierdlem51  31940  fourierdlem53  31942  fourierdlem64  31953  fourierdlem70  31959  fourierdlem71  31960  fourierdlem76  31965  fourierdlem78  31967  fourierdlem79  31968  fourierdlem80  31969  fourierdlem93  31982  fourierdlem97  31986  fourierdlem103  31992  fourierdlem104  31993  pmapglb  35494  hdmapoc  37661

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