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

Theorem dfss3 3433
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 3432 . 2  |-  ( A 
C_  B  <->  A. x
( x  e.  A  ->  x  e.  B ) )
2 df-ral 2753 . 2  |-  ( A. x  e.  A  x  e.  B  <->  A. x ( x  e.  A  ->  x  e.  B ) )
31, 2bitr4i 260 1  |-  ( A 
C_  B  <->  A. x  e.  A  x  e.  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189   A.wal 1452    e. wcel 1897   A.wral 2748    C_ wss 3415
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441
This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-ral 2753  df-in 3422  df-ss 3429
This theorem is referenced by:  ssrab  3518  elpwunsn  4023  eqsn  4145  uni0b  4236  uni0c  4237  ssint  4263  ssiinf  4340  sspwuni  4380  dftr3  4514  wefrc  4846  rninxp  5294  wfisg  5433  ordunisssuc  5543  fnres  5713  eqfnfv3  6000  funimass3  6020  ffvresb  6077  tfis  6707  smogt  7111  unifi  7888  unifi2  7889  fissuni  7904  fipreima  7905  cantnf  8223  tz9.12lem3  8285  r1elss  8302  rankval3b  8322  rankonidlem  8324  bndrank  8337  iscard  8434  cfub  8704  cflm  8705  fin1a2s  8869  dcomex  8902  ttukeylem6  8969  unirnfdomd  9017  alephreg  9032  tskord  9230  gruuni  9250  intgru  9264  grudomon  9267  axgroth3  9281  suplem1pr  9502  supexpr  9504  supsr  9561  hashfun  12641  4sqlem19  14961  imasaddfnlem  15482  imasvscafn  15491  setcepi  16031  acsfiindd  16471  sylow2blem3  17322  sylow3lem6  17332  efgval2  17422  iscyggen2  17564  iscyg3  17569  issubdrg  18081  isdomn2  18571  ishil2  19330  rintopn  19987  isbasis2g  20011  tgval2  20019  eltg2b  20022  tgss2  20051  basgen2  20053  bastop1  20057  intcld  20103  unicld  20109  isclo  20151  isclo2  20152  neips  20177  opnnei  20184  neiptopnei  20196  isperf3  20217  ssidcn  20319  ist1-3  20413  cmpcov2  20453  cmpsub  20463  2ndcdisj2  20520  txkgen  20715  xkoinjcn  20750  tgqtop  20775  flimopn  21038  flfnei  21054  tmdcn2  21152  qustgplem  21183  cfil3i  22287  cmetcaulem  22306  ovolfioo  22468  ovolficc  22469  ovolicc2lem4OLD  22521  ovolicc2lem4  22522  opnmblALT  22609  xrlimcnp  23942  ubthlem1  26560  hasheuni  28954  dmvlsiga  28999  ispisys2  29023  omssubadd  29176  omssubaddOLD  29180  eulerpartlemr  29255  eulerpartlemn  29262  cvmlift2lem1  30073  cvmlift2lem12  30085  mclsax  30255  setinds  30472  tfisg  30505  frinsg  30531  isfne4  31044  isfne2  31046  isfne3  31047  neibastop2lem  31064  filnetlem4  31085  fin2so  31976  poimirlem24  32008  poimirlem27  32011  nninfnub  32124  unichnidl  32308  ispridl2  32315  pmapglb  33379  hdmapoc  35546  isnacs2  35592  setindtrs  35924  dford3lem2  35926  dford3  35927  pwssfi  37418  ssdf  37460  disjf1o  37503  uzfissfz  37586  iuneqfzuzlem  37594  ssuzfz  37609  iccdificc  37678  fsumiunss  37691  limciccioolb  37738  limcicciooub  37754  limcresiooub  37760  icccncfext  37802  stoweidlem31  37929  stoweidlem39  37937  fourierdlem8  38014  fourierdlem27  38033  fourierdlem38  38045  fourierdlem40  38047  fourierdlem41  38048  fourierdlem46  38053  fourierdlem48  38055  fourierdlem49  38056  fourierdlem51  38058  fourierdlem53  38060  fourierdlem64  38071  fourierdlem70  38077  fourierdlem71  38078  fourierdlem76  38083  fourierdlem78  38085  fourierdlem79  38086  fourierdlem80  38087  fourierdlem93  38100  fourierdlem97  38104  fourierdlem103  38110  fourierdlem104  38111  rrxbasefi  38189  qndenserrn  38205  intsaluni  38225  salexct  38230  salgencntex  38239  gsumge0cl  38250  sge0fodjrnlem  38295  iundjiun  38335  meadjiunlem  38340  icoresmbl  38402  hoicvr  38407  hoidmv1le  38453  hoidmvlelem1  38454  hoidmvlelem3  38456  hoiqssbllem2  38482  hspmbllem2  38486  opnvonmbllem2  38492  dfss7  39021  uvtxanbgr  39513  nbupgruvtxres  39529  cplgruvtxb  39532  vdiscusgrb  39616
  Copyright terms: Public domain W3C validator