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

Theorem dfss3 3170
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 3169 . 2  |-  ( A 
C_  B  <->  A. x
( x  e.  A  ->  x  e.  B ) )
2 df-ral 2548 . 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 1527    e. wcel 1684   A.wral 2543    C_ wss 3152
This theorem is referenced by:  ssrab  3251  eqsn  3775  uni0b  3852  uni0c  3853  ssint  3878  ssiinf  3951  sspwuni  3987  dftr3  4117  wefrc  4387  ordunisssuc  4495  elpwunsn  4568  tfis  4645  rninxp  5117  fnres  5360  eqfnfv3  5624  funimass3  5641  ffvresb  5690  smogt  6384  unifi  7145  unifi2  7146  fissuni  7160  fipreima  7161  cantnf  7395  tz9.12lem3  7461  r1elss  7478  rankval3b  7498  rankonidlem  7500  bndrank  7513  iscard  7608  cfub  7875  cflm  7876  fin1a2s  8040  dcomex  8073  ttukeylem6  8141  unirnfdomd  8189  alephreg  8204  tskord  8402  gruuni  8422  intgru  8436  grudomon  8439  axgroth3  8453  suplem1pr  8676  supexpr  8678  supsr  8734  hashfun  11389  4sqlem19  13010  imasaddfnlem  13430  imasvscafn  13439  setcepi  13920  acsfiindd  14280  sylow2blem3  14933  sylow3lem6  14943  efgval2  15033  iscyggen2  15168  iscyg3  15173  issubdrg  15570  isdomn2  16040  ishil2  16619  rintopn  16655  isbasis2g  16686  tgval2  16694  eltg2b  16697  tgss2  16725  basgen2  16727  bastop1  16731  intcld  16777  unicld  16783  isclo  16824  isclo2  16825  neips  16850  opnnei  16857  isperf3  16884  ssidcn  16985  ist1-3  17077  cmpcov2  17117  cmpsub  17127  2ndcdisj2  17183  txkgen  17346  xkoinjcn  17381  tgqtop  17403  flimopn  17670  flfnei  17686  tmdcn2  17772  divstgplem  17803  cfil3i  18695  cmetcaulem  18714  ovolfioo  18827  ovolficc  18828  ovolicc2lem4  18879  opnmblALT  18958  xrlimcnp  20263  ubthlem1  21449  rnmpt2ss  23239  hasheuni  23453  dmvlsiga  23490  cvmlift2lem1  23833  cvmlift2lem12  23845  setinds  24134  tfisg  24204  wfisg  24209  frinsg  24245  domintrefb  25063  inttop3  25516  lemindclsbu  25995  iscol3  26094  isfne4  26269  isfne2  26271  isfne3  26272  neibastop2lem  26309  filnetlem4  26330  nninfnub  26461  unichnidl  26656  ispridl2  26663  isnacs2  26781  setindtrs  27118  dford3lem2  27120  dford3  27121  stoweidlem31  27780  stoweidlem39  27788  stirlinglem13  27835  pmapglb  29959  hdmapoc  32124
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-ral 2548  df-in 3159  df-ss 3166
  Copyright terms: Public domain W3C validator