MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dfss3 Structured version   Unicode version

Theorem dfss3 3487
Description: Alternate definition of subclass relationship. (Contributed by NM, 14-Oct-1999.)
Assertion
Ref Expression
dfss3  |-  ( A 
C_  B  <->  A. x  e.  A  x  e.  B )
Distinct variable groups:    x, A    x, B

Proof of Theorem dfss3
StepHypRef Expression
1 dfss2 3486 . 2  |-  ( A 
C_  B  <->  A. x
( x  e.  A  ->  x  e.  B ) )
2 df-ral 2812 . 2  |-  ( A. x  e.  A  x  e.  B  <->  A. x ( x  e.  A  ->  x  e.  B ) )
31, 2bitr4i 252 1  |-  ( A 
C_  B  <->  A. x  e.  A  x  e.  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184   A.wal 1372    e. wcel 1762   A.wral 2807    C_ wss 3469
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-ral 2812  df-in 3476  df-ss 3483
This theorem is referenced by:  ssrab  3571  elpwunsn  4061  eqsn  4181  uni0b  4263  uni0c  4264  ssint  4291  ssiinf  4367  sspwuni  4404  dftr3  4537  wefrc  4866  ordunisssuc  4973  rninxp  5437  fnres  5688  eqfnfv3  5968  funimass3  5988  ffvresb  6043  tfis  6660  smogt  7028  unifi  7798  unifi2  7799  fissuni  7814  fipreima  7815  cantnf  8101  cantnfOLD  8123  tz9.12lem3  8196  r1elss  8213  rankval3b  8233  rankonidlem  8235  bndrank  8248  iscard  8345  cfub  8618  cflm  8619  fin1a2s  8783  dcomex  8816  ttukeylem6  8883  unirnfdomd  8931  alephreg  8946  tskord  9147  gruuni  9167  intgru  9181  grudomon  9184  axgroth3  9198  suplem1pr  9419  supexpr  9421  supsr  9478  ssnn0fi  12050  hashfun  12448  4sqlem19  14329  imasaddfnlem  14772  imasvscafn  14781  setcepi  15262  acsfiindd  15653  sylow2blem3  16431  sylow3lem6  16441  efgval2  16531  iscyggen2  16668  iscyg3  16673  issubdrg  17230  isdomn2  17712  ishil2  18510  rintopn  19178  isbasis2g  19209  tgval2  19217  eltg2b  19220  tgss2  19248  basgen2  19250  bastop1  19254  intcld  19300  unicld  19306  isclo  19347  isclo2  19348  neips  19373  opnnei  19380  neiptopnei  19392  isperf3  19413  ssidcn  19515  ist1-3  19609  cmpcov2  19649  cmpsub  19659  2ndcdisj2  19717  txkgen  19881  xkoinjcn  19916  tgqtop  19941  flimopn  20204  flfnei  20220  tmdcn2  20316  divstgplem  20347  cfil3i  21436  cmetcaulem  21455  ovolfioo  21607  ovolficc  21608  ovolicc2lem4  21659  opnmblALT  21740  xrlimcnp  23019  ubthlem1  25312  hasheuni  27581  dmvlsiga  27619  eulerpartlemr  27803  eulerpartlemn  27810  cvmlift2lem1  28237  cvmlift2lem12  28249  setinds  28637  tfisg  28711  wfisg  28716  frinsg  28752  fin2so  29467  isfne4  29592  isfne2  29594  isfne3  29595  neibastop2lem  29632  filnetlem4  29653  nninfnub  29698  unichnidl  29882  ispridl2  29889  isnacs2  30093  setindtrs  30424  dford3lem2  30426  dford3  30427  icoiccdif  30947  limciccioolb  30982  limcicciooub  30998  limcresiooub  31003  icccncfext  31045  cncfiooicclem1  31051  itgperiod  31118  stoweidlem31  31150  stoweidlem39  31158  fourierdlem8  31234  fourierdlem27  31253  fourierdlem38  31264  fourierdlem40  31266  fourierdlem41  31267  fourierdlem46  31272  fourierdlem48  31274  fourierdlem49  31275  fourierdlem51  31277  fourierdlem53  31279  fourierdlem62  31288  fourierdlem64  31290  fourierdlem70  31296  fourierdlem71  31297  fourierdlem76  31302  fourierdlem78  31304  fourierdlem79  31305  fourierdlem80  31306  fourierdlem93  31319  fourierdlem97  31323  fourierdlem103  31329  fourierdlem104  31330  fouriersw  31351  pmapglb  34441  hdmapoc  36606
  Copyright terms: Public domain W3C validator