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

Theorem dfss3 3340
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 3339 . 2  |-  ( A 
C_  B  <->  A. x
( x  e.  A  ->  x  e.  B ) )
2 df-ral 2712 . 2  |-  ( A. x  e.  A  x  e.  B  <->  A. x ( x  e.  A  ->  x  e.  B ) )
31, 2bitr4i 245 1  |-  ( A 
C_  B  <->  A. x  e.  A  x  e.  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178   A.wal 1550    e. wcel 1726   A.wral 2707    C_ wss 3322
This theorem is referenced by:  ssrab  3423  eqsn  3962  uni0b  4042  uni0c  4043  ssint  4068  ssiinf  4142  sspwuni  4179  dftr3  4309  wefrc  4579  ordunisssuc  4687  elpwunsn  4760  tfis  4837  rninxp  5313  fnres  5564  eqfnfv3  5832  funimass3  5849  ffvresb  5903  smogt  6632  unifi  7398  unifi2  7399  fissuni  7414  fipreima  7415  cantnf  7652  tz9.12lem3  7718  r1elss  7735  rankval3b  7755  rankonidlem  7757  bndrank  7770  iscard  7867  cfub  8134  cflm  8135  fin1a2s  8299  dcomex  8332  ttukeylem6  8399  unirnfdomd  8447  alephreg  8462  tskord  8660  gruuni  8680  intgru  8694  grudomon  8697  axgroth3  8711  suplem1pr  8934  supexpr  8936  supsr  8992  hashfun  11705  4sqlem19  13336  imasaddfnlem  13758  imasvscafn  13767  setcepi  14248  acsfiindd  14608  sylow2blem3  15261  sylow3lem6  15271  efgval2  15361  iscyggen2  15496  iscyg3  15501  issubdrg  15898  isdomn2  16364  ishil2  16951  rintopn  16987  isbasis2g  17018  tgval2  17026  eltg2b  17029  tgss2  17057  basgen2  17059  bastop1  17063  intcld  17109  unicld  17115  isclo  17156  isclo2  17157  neips  17182  opnnei  17189  neiptopnei  17201  isperf3  17222  ssidcn  17324  ist1-3  17418  cmpcov2  17458  cmpsub  17468  2ndcdisj2  17525  txkgen  17689  xkoinjcn  17724  tgqtop  17749  flimopn  18012  flfnei  18028  tmdcn2  18124  divstgplem  18155  cfil3i  19227  cmetcaulem  19246  ovolfioo  19369  ovolficc  19370  ovolicc2lem4  19421  opnmblALT  19500  xrlimcnp  20812  ubthlem1  22377  hasheuni  24480  dmvlsiga  24517  cvmlift2lem1  24994  cvmlift2lem12  25006  setinds  25410  tfisg  25484  wfisg  25489  frinsg  25525  isfne4  26363  isfne2  26365  isfne3  26366  neibastop2lem  26403  filnetlem4  26424  nninfnub  26469  unichnidl  26655  ispridl2  26662  isnacs2  26774  setindtrs  27110  dford3lem2  27112  dford3  27113  stoweidlem31  27770  stoweidlem39  27778  pmapglb  30641  hdmapoc  32806
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-ral 2712  df-in 3329  df-ss 3336
  Copyright terms: Public domain W3C validator