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

Theorem dfss3 3183
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 3182 . 2  |-  ( A 
C_  B  <->  A. x
( x  e.  A  ->  x  e.  B ) )
2 df-ral 2561 . 2  |-  ( A. x  e.  A  x  e.  B  <->  A. x ( x  e.  A  ->  x  e.  B ) )
31, 2bitr4i 243 1  |-  ( A 
C_  B  <->  A. x  e.  A  x  e.  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176   A.wal 1530    e. wcel 1696   A.wral 2556    C_ wss 3165
This theorem is referenced by:  ssrab  3264  eqsn  3791  uni0b  3868  uni0c  3869  ssint  3894  ssiinf  3967  sspwuni  4003  dftr3  4133  wefrc  4403  ordunisssuc  4511  elpwunsn  4584  tfis  4661  rninxp  5133  fnres  5376  eqfnfv3  5640  funimass3  5657  ffvresb  5706  smogt  6400  unifi  7161  unifi2  7162  fissuni  7176  fipreima  7177  cantnf  7411  tz9.12lem3  7477  r1elss  7494  rankval3b  7514  rankonidlem  7516  bndrank  7529  iscard  7624  cfub  7891  cflm  7892  fin1a2s  8056  dcomex  8089  ttukeylem6  8157  unirnfdomd  8205  alephreg  8220  tskord  8418  gruuni  8438  intgru  8452  grudomon  8455  axgroth3  8469  suplem1pr  8692  supexpr  8694  supsr  8750  hashfun  11405  4sqlem19  13026  imasaddfnlem  13446  imasvscafn  13455  setcepi  13936  acsfiindd  14296  sylow2blem3  14949  sylow3lem6  14959  efgval2  15049  iscyggen2  15184  iscyg3  15189  issubdrg  15586  isdomn2  16056  ishil2  16635  rintopn  16671  isbasis2g  16702  tgval2  16710  eltg2b  16713  tgss2  16741  basgen2  16743  bastop1  16747  intcld  16793  unicld  16799  isclo  16840  isclo2  16841  neips  16866  opnnei  16873  isperf3  16900  ssidcn  17001  ist1-3  17093  cmpcov2  17133  cmpsub  17143  2ndcdisj2  17199  txkgen  17362  xkoinjcn  17397  tgqtop  17419  flimopn  17686  flfnei  17702  tmdcn2  17788  divstgplem  17819  cfil3i  18711  cmetcaulem  18730  ovolfioo  18843  ovolficc  18844  ovolicc2lem4  18895  opnmblALT  18974  xrlimcnp  20279  ubthlem1  21465  rnmpt2ss  23254  hasheuni  23468  dmvlsiga  23505  cvmlift2lem1  23848  cvmlift2lem12  23860  setinds  24205  tfisg  24275  wfisg  24280  frinsg  24316  domintrefb  25166  inttop3  25619  lemindclsbu  26098  iscol3  26197  isfne4  26372  isfne2  26374  isfne3  26375  neibastop2lem  26412  filnetlem4  26433  nninfnub  26564  unichnidl  26759  ispridl2  26766  isnacs2  26884  setindtrs  27221  dford3lem2  27223  dford3  27224  stoweidlem31  27883  stoweidlem39  27891  stirlinglem13  27938  pmapglb  30581  hdmapoc  32746
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-ral 2561  df-in 3172  df-ss 3179
  Copyright terms: Public domain W3C validator