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

Theorem dfss3 3479
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 3478 . 2  |-  ( A 
C_  B  <->  A. x
( x  e.  A  ->  x  e.  B ) )
2 df-ral 2809 . 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 1396    e. wcel 1823   A.wral 2804    C_ wss 3461
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-ral 2809  df-in 3468  df-ss 3475
This theorem is referenced by:  ssrab  3564  elpwunsn  4057  eqsn  4177  uni0b  4260  uni0c  4261  ssint  4287  ssiinf  4364  sspwuni  4404  dftr3  4536  wefrc  4862  ordunisssuc  4969  rninxp  5431  fnres  5679  eqfnfv3  5959  funimass3  5979  ffvresb  6038  tfis  6662  smogt  7030  unifi  7801  unifi2  7802  fissuni  7817  fipreima  7818  cantnf  8103  cantnfOLD  8125  tz9.12lem3  8198  r1elss  8215  rankval3b  8235  rankonidlem  8237  bndrank  8250  iscard  8347  cfub  8620  cflm  8621  fin1a2s  8785  dcomex  8818  ttukeylem6  8885  unirnfdomd  8933  alephreg  8948  tskord  9147  gruuni  9167  intgru  9181  grudomon  9184  axgroth3  9198  suplem1pr  9419  supexpr  9421  supsr  9478  hashfun  12479  4sqlem19  14565  imasaddfnlem  15017  imasvscafn  15026  setcepi  15566  acsfiindd  16006  sylow2blem3  16841  sylow3lem6  16851  efgval2  16941  iscyggen2  17083  iscyg3  17088  issubdrg  17649  isdomn2  18143  ishil2  18923  rintopn  19585  isbasis2g  19616  tgval2  19624  eltg2b  19627  tgss2  19656  basgen2  19658  bastop1  19662  intcld  19708  unicld  19714  isclo  19755  isclo2  19756  neips  19781  opnnei  19788  neiptopnei  19800  isperf3  19821  ssidcn  19923  ist1-3  20017  cmpcov2  20057  cmpsub  20067  2ndcdisj2  20124  txkgen  20319  xkoinjcn  20354  tgqtop  20379  flimopn  20642  flfnei  20658  tmdcn2  20754  qustgplem  20785  cfil3i  21874  cmetcaulem  21893  ovolfioo  22045  ovolficc  22046  ovolicc2lem4  22097  opnmblALT  22178  xrlimcnp  23496  ubthlem1  25984  hasheuni  28314  dmvlsiga  28359  ispisys2  28383  omssubadd  28508  eulerpartlemr  28577  eulerpartlemn  28584  cvmlift2lem1  29011  cvmlift2lem12  29023  mclsax  29193  setinds  29450  tfisg  29524  wfisg  29529  frinsg  29565  fin2so  30280  isfne4  30398  isfne2  30400  isfne3  30401  neibastop2lem  30418  filnetlem4  30439  nninfnub  30484  unichnidl  30668  ispridl2  30675  isnacs2  30878  setindtrs  31206  dford3lem2  31208  dford3  31209  limciccioolb  31866  limcicciooub  31882  limcresiooub  31887  icccncfext  31929  stoweidlem31  32052  stoweidlem39  32060  fourierdlem8  32136  fourierdlem27  32155  fourierdlem38  32166  fourierdlem40  32168  fourierdlem41  32169  fourierdlem46  32174  fourierdlem48  32176  fourierdlem49  32177  fourierdlem51  32179  fourierdlem53  32181  fourierdlem64  32192  fourierdlem70  32198  fourierdlem71  32199  fourierdlem76  32204  fourierdlem78  32206  fourierdlem79  32207  fourierdlem80  32208  fourierdlem93  32221  fourierdlem97  32225  fourierdlem103  32231  fourierdlem104  32232  pmapglb  35891  hdmapoc  38058
  Copyright terms: Public domain W3C validator