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

Theorem dfss3 3476
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 3475 . 2  |-  ( A 
C_  B  <->  A. x
( x  e.  A  ->  x  e.  B ) )
2 df-ral 2796 . 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 1379    e. wcel 1802   A.wral 2791    C_ wss 3458
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-ral 2796  df-in 3465  df-ss 3472
This theorem is referenced by:  ssrab  3560  elpwunsn  4051  eqsn  4172  uni0b  4255  uni0c  4256  ssint  4283  ssiinf  4360  sspwuni  4397  dftr3  4530  wefrc  4859  ordunisssuc  4966  rninxp  5432  fnres  5683  eqfnfv3  5964  funimass3  5984  ffvresb  6043  tfis  6670  smogt  7036  unifi  7807  unifi2  7808  fissuni  7823  fipreima  7824  cantnf  8110  cantnfOLD  8132  tz9.12lem3  8205  r1elss  8222  rankval3b  8242  rankonidlem  8244  bndrank  8257  iscard  8354  cfub  8627  cflm  8628  fin1a2s  8792  dcomex  8825  ttukeylem6  8892  unirnfdomd  8940  alephreg  8955  tskord  9156  gruuni  9176  intgru  9190  grudomon  9193  axgroth3  9207  suplem1pr  9428  supexpr  9430  supsr  9487  hashfun  12469  4sqlem19  14353  imasaddfnlem  14797  imasvscafn  14806  setcepi  15284  acsfiindd  15676  sylow2blem3  16511  sylow3lem6  16521  efgval2  16611  iscyggen2  16753  iscyg3  16758  issubdrg  17322  isdomn2  17816  ishil2  18617  rintopn  19285  isbasis2g  19316  tgval2  19324  eltg2b  19327  tgss2  19355  basgen2  19357  bastop1  19361  intcld  19407  unicld  19413  isclo  19454  isclo2  19455  neips  19480  opnnei  19487  neiptopnei  19499  isperf3  19520  ssidcn  19622  ist1-3  19716  cmpcov2  19756  cmpsub  19766  2ndcdisj2  19824  txkgen  20019  xkoinjcn  20054  tgqtop  20079  flimopn  20342  flfnei  20358  tmdcn2  20454  qustgplem  20485  cfil3i  21574  cmetcaulem  21593  ovolfioo  21745  ovolficc  21746  ovolicc2lem4  21797  opnmblALT  21878  xrlimcnp  23163  ubthlem1  25651  hasheuni  27957  dmvlsiga  27995  eulerpartlemr  28179  eulerpartlemn  28186  cvmlift2lem1  28613  cvmlift2lem12  28625  mclsax  28795  setinds  29178  tfisg  29252  wfisg  29257  frinsg  29293  fin2so  30008  isfne4  30126  isfne2  30128  isfne3  30129  neibastop2lem  30146  filnetlem4  30167  nninfnub  30212  unichnidl  30396  ispridl2  30403  isnacs2  30606  setindtrs  30935  dford3lem2  30937  dford3  30938  limciccioolb  31531  limcicciooub  31547  limcresiooub  31552  icccncfext  31593  stoweidlem31  31698  stoweidlem39  31706  fourierdlem8  31782  fourierdlem27  31801  fourierdlem38  31812  fourierdlem40  31814  fourierdlem41  31815  fourierdlem46  31820  fourierdlem48  31822  fourierdlem49  31823  fourierdlem51  31825  fourierdlem53  31827  fourierdlem64  31838  fourierdlem70  31844  fourierdlem71  31845  fourierdlem76  31850  fourierdlem78  31852  fourierdlem79  31853  fourierdlem80  31854  fourierdlem93  31867  fourierdlem97  31871  fourierdlem103  31877  fourierdlem104  31878  pmapglb  35196  hdmapoc  37363
  Copyright terms: Public domain W3C validator