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

Theorem dfss3 3392
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 3391 . 2  |-  ( A 
C_  B  <->  A. x
( x  e.  A  ->  x  e.  B ) )
2 df-ral 2714 . 2  |-  ( A. x  e.  A  x  e.  B  <->  A. x ( x  e.  A  ->  x  e.  B ) )
31, 2bitr4i 255 1  |-  ( A 
C_  B  <->  A. x  e.  A  x  e.  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187   A.wal 1435    e. wcel 1872   A.wral 2709    C_ wss 3374
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2403
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2410  df-cleq 2416  df-clel 2419  df-ral 2714  df-in 3381  df-ss 3388
This theorem is referenced by:  ssrab  3477  elpwunsn  3978  eqsn  4099  uni0b  4182  uni0c  4183  ssint  4209  ssiinf  4286  sspwuni  4326  dftr3  4460  wefrc  4785  rninxp  5233  wfisg  5372  ordunisssuc  5482  fnres  5648  eqfnfv3  5932  funimass3  5952  ffvresb  6008  tfis  6634  smogt  7036  unifi  7811  unifi2  7812  fissuni  7827  fipreima  7828  cantnf  8145  tz9.12lem3  8207  r1elss  8224  rankval3b  8244  rankonidlem  8246  bndrank  8259  iscard  8356  cfub  8625  cflm  8626  fin1a2s  8790  dcomex  8823  ttukeylem6  8890  unirnfdomd  8938  alephreg  8953  tskord  9151  gruuni  9171  intgru  9185  grudomon  9188  axgroth3  9202  suplem1pr  9423  supexpr  9425  supsr  9482  hashfun  12552  4sqlem19  14851  imasaddfnlem  15372  imasvscafn  15381  setcepi  15921  acsfiindd  16361  sylow2blem3  17212  sylow3lem6  17222  efgval2  17312  iscyggen2  17454  iscyg3  17459  issubdrg  17971  isdomn2  18461  ishil2  19219  rintopn  19876  isbasis2g  19900  tgval2  19908  eltg2b  19911  tgss2  19940  basgen2  19942  bastop1  19946  intcld  19992  unicld  19998  isclo  20040  isclo2  20041  neips  20066  opnnei  20073  neiptopnei  20085  isperf3  20106  ssidcn  20208  ist1-3  20302  cmpcov2  20342  cmpsub  20352  2ndcdisj2  20409  txkgen  20604  xkoinjcn  20639  tgqtop  20664  flimopn  20927  flfnei  20943  tmdcn2  21041  qustgplem  21072  cfil3i  22176  cmetcaulem  22195  ovolfioo  22357  ovolficc  22358  ovolicc2lem4OLD  22410  ovolicc2lem4  22411  opnmblALT  22498  xrlimcnp  23831  ubthlem1  26449  hasheuni  28853  dmvlsiga  28898  ispisys2  28922  omssubadd  29075  omssubaddOLD  29079  eulerpartlemr  29154  eulerpartlemn  29161  cvmlift2lem1  29972  cvmlift2lem12  29984  mclsax  30154  setinds  30370  tfisg  30403  frinsg  30429  isfne4  30940  isfne2  30942  isfne3  30943  neibastop2lem  30960  filnetlem4  30981  fin2so  31839  poimirlem24  31871  poimirlem27  31874  nninfnub  31987  unichnidl  32171  ispridl2  32178  pmapglb  33247  hdmapoc  35414  isnacs2  35460  setindtrs  35793  dford3lem2  35795  dford3  35796  pwssfi  37297  disjf1o  37370  uzfissfz  37446  iuneqfzuzlem  37454  ssuzfz  37469  fsumiunss  37538  limciccioolb  37584  limcicciooub  37600  limcresiooub  37606  icccncfext  37648  stoweidlem31  37775  stoweidlem39  37783  fourierdlem8  37860  fourierdlem27  37879  fourierdlem38  37891  fourierdlem40  37893  fourierdlem41  37894  fourierdlem46  37899  fourierdlem48  37901  fourierdlem49  37902  fourierdlem51  37904  fourierdlem53  37906  fourierdlem64  37917  fourierdlem70  37923  fourierdlem71  37924  fourierdlem76  37929  fourierdlem78  37931  fourierdlem79  37932  fourierdlem80  37933  fourierdlem93  37946  fourierdlem97  37950  fourierdlem103  37956  fourierdlem104  37957  intsaluni  38052  gsumge0cl  38064  sge0fodjrnlem  38109  iundjiun  38149  meadjiunlem  38154  icoresmbl  38212  hoicvr  38217  hoidmv1le  38263  hoidmvlelem1  38264  hoidmvlelem3  38266  dfss7  38795  uvtxanbgr  39194  nbupgruvtxres  39208  cplgruvtxb  39211
  Copyright terms: Public domain W3C validator