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

Theorem dfss3 3444
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 3443 . 2  |-  ( A 
C_  B  <->  A. x
( x  e.  A  ->  x  e.  B ) )
2 df-ral 2800 . 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 1368    e. wcel 1758   A.wral 2795    C_ wss 3426
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-ral 2800  df-in 3433  df-ss 3440
This theorem is referenced by:  ssrab  3528  elpwunsn  4015  eqsn  4132  uni0b  4214  uni0c  4215  ssint  4242  ssiinf  4317  sspwuni  4354  dftr3  4487  wefrc  4812  ordunisssuc  4919  rninxp  5375  fnres  5625  eqfnfv3  5898  funimass3  5918  ffvresb  5973  tfis  6565  smogt  6928  unifi  7701  unifi2  7702  fissuni  7717  fipreima  7718  cantnf  8002  cantnfOLD  8024  tz9.12lem3  8097  r1elss  8114  rankval3b  8134  rankonidlem  8136  bndrank  8149  iscard  8246  cfub  8519  cflm  8520  fin1a2s  8684  dcomex  8717  ttukeylem6  8784  unirnfdomd  8832  alephreg  8847  tskord  9048  gruuni  9068  intgru  9082  grudomon  9085  axgroth3  9099  suplem1pr  9322  supexpr  9324  supsr  9380  hashfun  12301  4sqlem19  14126  imasaddfnlem  14568  imasvscafn  14577  setcepi  15058  acsfiindd  15449  sylow2blem3  16225  sylow3lem6  16235  efgval2  16325  iscyggen2  16462  iscyg3  16467  issubdrg  16996  isdomn2  17477  ishil2  18253  rintopn  18638  isbasis2g  18669  tgval2  18677  eltg2b  18680  tgss2  18708  basgen2  18710  bastop1  18714  intcld  18760  unicld  18766  isclo  18807  isclo2  18808  neips  18833  opnnei  18840  neiptopnei  18852  isperf3  18873  ssidcn  18975  ist1-3  19069  cmpcov2  19109  cmpsub  19119  2ndcdisj2  19177  txkgen  19341  xkoinjcn  19376  tgqtop  19401  flimopn  19664  flfnei  19680  tmdcn2  19776  divstgplem  19807  cfil3i  20896  cmetcaulem  20915  ovolfioo  21067  ovolficc  21068  ovolicc2lem4  21119  opnmblALT  21199  xrlimcnp  22478  ubthlem1  24406  hasheuni  26668  dmvlsiga  26706  eulerpartlemr  26891  eulerpartlemn  26898  cvmlift2lem1  27325  cvmlift2lem12  27337  setinds  27725  tfisg  27799  wfisg  27804  frinsg  27840  fin2so  28554  isfne4  28679  isfne2  28681  isfne3  28682  neibastop2lem  28719  filnetlem4  28740  nninfnub  28785  unichnidl  28969  ispridl2  28976  isnacs2  29180  setindtrs  29512  dford3lem2  29514  dford3  29515  stoweidlem31  29964  stoweidlem39  29972  ssnn0fi  30884  pmapglb  33720  hdmapoc  35885
  Copyright terms: Public domain W3C validator