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

Theorem dfss3 3334
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 3333 . 2  |-  ( A 
C_  B  <->  A. x
( x  e.  A  ->  x  e.  B ) )
2 df-ral 2710 . 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 1360    e. wcel 1755   A.wral 2705    C_ wss 3316
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-ral 2710  df-in 3323  df-ss 3330
This theorem is referenced by:  ssrab  3418  elpwunsn  3905  eqsn  4022  uni0b  4104  uni0c  4105  ssint  4132  ssiinf  4207  sspwuni  4244  dftr3  4377  wefrc  4701  ordunisssuc  4808  rninxp  5265  fnres  5515  eqfnfv3  5787  funimass3  5807  ffvresb  5861  tfis  6454  smogt  6814  unifi  7588  unifi2  7589  fissuni  7604  fipreima  7605  cantnf  7889  cantnfOLD  7911  tz9.12lem3  7984  r1elss  8001  rankval3b  8021  rankonidlem  8023  bndrank  8036  iscard  8133  cfub  8406  cflm  8407  fin1a2s  8571  dcomex  8604  ttukeylem6  8671  unirnfdomd  8719  alephreg  8734  tskord  8935  gruuni  8955  intgru  8969  grudomon  8972  axgroth3  8986  suplem1pr  9209  supexpr  9211  supsr  9267  hashfun  12183  4sqlem19  14007  imasaddfnlem  14449  imasvscafn  14458  setcepi  14939  acsfiindd  15330  sylow2blem3  16101  sylow3lem6  16111  efgval2  16201  iscyggen2  16338  iscyg3  16343  issubdrg  16814  isdomn2  17293  ishil2  17986  rintopn  18364  isbasis2g  18395  tgval2  18403  eltg2b  18406  tgss2  18434  basgen2  18436  bastop1  18440  intcld  18486  unicld  18492  isclo  18533  isclo2  18534  neips  18559  opnnei  18566  neiptopnei  18578  isperf3  18599  ssidcn  18701  ist1-3  18795  cmpcov2  18835  cmpsub  18845  2ndcdisj2  18903  txkgen  19067  xkoinjcn  19102  tgqtop  19127  flimopn  19390  flfnei  19406  tmdcn2  19502  divstgplem  19533  cfil3i  20622  cmetcaulem  20641  ovolfioo  20793  ovolficc  20794  ovolicc2lem4  20845  opnmblALT  20925  xrlimcnp  22247  ubthlem1  24094  hasheuni  26388  dmvlsiga  26426  eulerpartlemr  26605  eulerpartlemn  26612  cvmlift2lem1  27039  cvmlift2lem12  27051  setinds  27438  tfisg  27512  wfisg  27517  frinsg  27553  fin2so  28260  isfne4  28385  isfne2  28387  isfne3  28388  neibastop2lem  28425  filnetlem4  28446  nninfnub  28491  unichnidl  28675  ispridl2  28682  isnacs2  28887  setindtrs  29219  dford3lem2  29221  dford3  29222  areaquad  29437  stoweidlem31  29672  stoweidlem39  29680  pmapglb  32987  hdmapoc  35152
  Copyright terms: Public domain W3C validator