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

Theorem dfss3 3330
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 3329 . 2  |-  ( A 
C_  B  <->  A. x
( x  e.  A  ->  x  e.  B ) )
2 df-ral 2702 . 2  |-  ( A. x  e.  A  x  e.  B  <->  A. x ( x  e.  A  ->  x  e.  B ) )
31, 2bitr4i 244 1  |-  ( A 
C_  B  <->  A. x  e.  A  x  e.  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177   A.wal 1549    e. wcel 1725   A.wral 2697    C_ wss 3312
This theorem is referenced by:  ssrab  3413  eqsn  3952  uni0b  4032  uni0c  4033  ssint  4058  ssiinf  4132  sspwuni  4168  dftr3  4298  wefrc  4568  ordunisssuc  4676  elpwunsn  4749  tfis  4826  rninxp  5302  fnres  5553  eqfnfv3  5821  funimass3  5838  ffvresb  5892  smogt  6621  unifi  7387  unifi2  7388  fissuni  7403  fipreima  7404  cantnf  7641  tz9.12lem3  7707  r1elss  7724  rankval3b  7744  rankonidlem  7746  bndrank  7759  iscard  7854  cfub  8121  cflm  8122  fin1a2s  8286  dcomex  8319  ttukeylem6  8386  unirnfdomd  8434  alephreg  8449  tskord  8647  gruuni  8667  intgru  8681  grudomon  8684  axgroth3  8698  suplem1pr  8921  supexpr  8923  supsr  8979  hashfun  11692  4sqlem19  13323  imasaddfnlem  13745  imasvscafn  13754  setcepi  14235  acsfiindd  14595  sylow2blem3  15248  sylow3lem6  15258  efgval2  15348  iscyggen2  15483  iscyg3  15488  issubdrg  15885  isdomn2  16351  ishil2  16938  rintopn  16974  isbasis2g  17005  tgval2  17013  eltg2b  17016  tgss2  17044  basgen2  17046  bastop1  17050  intcld  17096  unicld  17102  isclo  17143  isclo2  17144  neips  17169  opnnei  17176  neiptopnei  17188  isperf3  17209  ssidcn  17311  ist1-3  17405  cmpcov2  17445  cmpsub  17455  2ndcdisj2  17512  txkgen  17676  xkoinjcn  17711  tgqtop  17736  flimopn  17999  flfnei  18015  tmdcn2  18111  divstgplem  18142  cfil3i  19214  cmetcaulem  19233  ovolfioo  19356  ovolficc  19357  ovolicc2lem4  19408  opnmblALT  19487  xrlimcnp  20799  ubthlem1  22364  hasheuni  24467  dmvlsiga  24504  cvmlift2lem1  24981  cvmlift2lem12  24993  setinds  25397  tfisg  25471  wfisg  25476  frinsg  25512  isfne4  26340  isfne2  26342  isfne3  26343  neibastop2lem  26380  filnetlem4  26401  nninfnub  26446  unichnidl  26632  ispridl2  26639  isnacs2  26751  setindtrs  27087  dford3lem2  27089  dford3  27090  stoweidlem31  27747  stoweidlem39  27755  pmapglb  30504  hdmapoc  32669
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-ral 2702  df-in 3319  df-ss 3326
  Copyright terms: Public domain W3C validator