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

Theorem dfss3 3341
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 3340 . 2  |-  ( A 
C_  B  <->  A. x
( x  e.  A  ->  x  e.  B ) )
2 df-ral 2715 . 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 1367    e. wcel 1756   A.wral 2710    C_ wss 3323
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-ral 2715  df-in 3330  df-ss 3337
This theorem is referenced by:  ssrab  3425  elpwunsn  3912  eqsn  4029  uni0b  4111  uni0c  4112  ssint  4139  ssiinf  4214  sspwuni  4251  dftr3  4384  wefrc  4709  ordunisssuc  4816  rninxp  5272  fnres  5522  eqfnfv3  5794  funimass3  5814  ffvresb  5869  tfis  6460  smogt  6820  unifi  7592  unifi2  7593  fissuni  7608  fipreima  7609  cantnf  7893  cantnfOLD  7915  tz9.12lem3  7988  r1elss  8005  rankval3b  8025  rankonidlem  8027  bndrank  8040  iscard  8137  cfub  8410  cflm  8411  fin1a2s  8575  dcomex  8608  ttukeylem6  8675  unirnfdomd  8723  alephreg  8738  tskord  8939  gruuni  8959  intgru  8973  grudomon  8976  axgroth3  8990  suplem1pr  9213  supexpr  9215  supsr  9271  hashfun  12191  4sqlem19  14016  imasaddfnlem  14458  imasvscafn  14467  setcepi  14948  acsfiindd  15339  sylow2blem3  16112  sylow3lem6  16122  efgval2  16212  iscyggen2  16349  iscyg3  16354  issubdrg  16870  isdomn2  17351  ishil2  18124  rintopn  18502  isbasis2g  18533  tgval2  18541  eltg2b  18544  tgss2  18572  basgen2  18574  bastop1  18578  intcld  18624  unicld  18630  isclo  18671  isclo2  18672  neips  18697  opnnei  18704  neiptopnei  18716  isperf3  18737  ssidcn  18839  ist1-3  18933  cmpcov2  18973  cmpsub  18983  2ndcdisj2  19041  txkgen  19205  xkoinjcn  19240  tgqtop  19265  flimopn  19528  flfnei  19544  tmdcn2  19640  divstgplem  19671  cfil3i  20760  cmetcaulem  20779  ovolfioo  20931  ovolficc  20932  ovolicc2lem4  20983  opnmblALT  21063  xrlimcnp  22342  ubthlem1  24239  hasheuni  26503  dmvlsiga  26541  eulerpartlemr  26726  eulerpartlemn  26733  cvmlift2lem1  27160  cvmlift2lem12  27172  setinds  27560  tfisg  27634  wfisg  27639  frinsg  27675  fin2so  28387  isfne4  28512  isfne2  28514  isfne3  28515  neibastop2lem  28552  filnetlem4  28573  nninfnub  28618  unichnidl  28802  ispridl2  28809  isnacs2  29013  setindtrs  29345  dford3lem2  29347  dford3  29348  stoweidlem31  29797  stoweidlem39  29805  ssnn0fi  30715  pmapglb  33307  hdmapoc  35472
  Copyright terms: Public domain W3C validator