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

Theorem cbvrexv 3089
Description: Change the bound variable of a restricted existential quantifier using implicit substitution. (Contributed by NM, 2-Jun-1998.)
Hypothesis
Ref Expression
cbvralv.1  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
Assertion
Ref Expression
cbvrexv  |-  ( E. x  e.  A  ph  <->  E. y  e.  A  ps )
Distinct variable groups:    x, A    y, A    ph, y    ps, x
Allowed substitution hints:    ph( x)    ps( y)

Proof of Theorem cbvrexv
StepHypRef Expression
1 nfv 1683 . 2  |-  F/ y
ph
2 nfv 1683 . 2  |-  F/ x ps
3 cbvralv.1 . 2  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
41, 2, 3cbvrex 3085 1  |-  ( E. x  e.  A  ph  <->  E. y  e.  A  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184   E.wrex 2815
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-ex 1597  df-nf 1600  df-sb 1712  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ral 2819  df-rex 2820
This theorem is referenced by:  cbvrex2v  3097  reu7  3298  reusv3  4655  xpdifid  5433  fliftfun  6196  grpridd  6497  funcnvuni  6734  fun11iun  6741  nneob  7298  pssnn  7735  frfi  7761  finsschain  7823  marypha1lem  7889  supmo  7908  suplub2  7917  ordtypelem3  7941  ordtypelem9  7947  wemaplem1  7967  brwdom3  8004  unwdomg  8006  cantnf  8108  cantnfOLD  8130  trcl  8155  infxpenc2  8395  infxpenc2OLD  8399  aceq2  8496  dfac5lem4  8503  kmlem9  8534  kmlem14  8539  fin23lem26  8701  fin1a2lem13  8788  axdc3lem3  8828  winainflem  9067  axgroth4  9206  suprlub  10501  supmul1  10504  supmullem1  10505  supmullem2  10506  supmul  10507  ublbneg  11162  zsupss  11167  xrsupsslem  11494  xrinfmsslem  11495  fsuppmapnn0fiub  12061  rexanre  13138  rexuzre  13144  rexico  13145  caurcvg2  13459  caucvgb  13461  summolem2  13497  summo  13498  mertens  13654  odd2np1lem  13900  gcdcllem1  14004  pceu  14225  4sqlem12  14329  vdwlem10  14363  vdwlem13  14366  vdwnn  14371  drsdirfi  15421  gaorb  16140  psgnunilem3  16317  psgnunilem4  16318  psgneu  16327  pj1eu  16510  efgsfo  16553  cyggeninv  16677  cygabl  16684  pgpfac1lem5  16920  pgpfac1  16921  pgpfaclem2  16923  lss1d  17392  lspsneq  17551  lspsolvlem  17571  lbsextlem2  17588  mplcoe5lem  17901  cygznlem3  18375  pmatcollpw3fi1lem2  19055  ordtrest2lem  19470  cnprest  19556  1stcfb  19712  1stcelcls  19728  elpt  19808  fbssfi  20073  fgcl  20114  rnelfmlem  20188  fmfnfmlem3  20192  txflf  20242  alexsubb  20281  alexsubALTlem4  20285  isucn2  20517  icccmplem2  21063  ply1divex  22272  coeeu  22357  plydivex  22427  aannenlem2  22459  ulmcau  22524  ulmbdd  22527  dchrptlem2  23268  bposlem9  23295  pntibndlem3  23505  pntlemi  23517  pntlemp  23523  pntleml  23524  pnt3  23525  legval  23698  legov  23699  legov2  23700  erclwwlksym  24490  erclwwlktr  24491  erclwwlknsym  24502  erclwwlkntr  24503  eleclclwwlkn  24509  hashecclwwlkn1  24510  usghashecclwwlk  24511  frgraregorufr0  24729  isgrpo2  24875  grpoidinvlem3  24884  isgrp2d  24913  isgrpda  24975  ubthlem3  25464  norm1exi  25844  pjhthmo  25896  cdjreui  27027  cdj3i  27036  isarchi3  27393  archiabl  27404  ordtrest2NEWlem  27540  lmxrge0  27570  esumcvg  27732  eulerpartlems  27939  eulerpartlemgvv  27955  conpcon  28320  cvmlift2lem12  28399  cvmlift2lem13  28400  cvmlift3lem2  28405  cvmlift3lem7  28410  cvmlift3  28413  prodmolem2  28644  prodmo  28645  poseq  28910  soseq  28911  funtransport  29258  funray  29367  funline  29369  supaddc  29618  supadd  29619  ptrest  29625  ismblfin  29632  volsupnfl  29636  itg2addnclem  29643  fnessref  29765  neibastop2  29782  unirep  29806  filbcmb  29834  sdclem1  29839  sdc  29840  fdc  29841  incsequz  29844  heibor1lem  29908  heiborlem10  29919  isdrngo2  29964  prnc  30067  prtlem13  30213  prtlem15  30220  mzpcompact2lem  30288  eldioph3  30303  diophrex  30313  rexrabdioph  30331  eldioph4i  30350  aomclem8  30611  hbtlem2  30677  rngunsnply  30727  dvconstbi  30839  expgrowth  30840  limsupre  31183  cncfshiftioo  31231  itgiccshift  31298  itgperiod  31299  fourierdlem42  31449  fourierdlem48  31455  fourierdlem96  31503  fourierdlem97  31504  fourierdlem98  31505  fourierdlem99  31506  fourierdlem105  31512  fourierdlem108  31515  fourierdlem110  31517  fourierdlem112  31519  fourierdlem113  31520  lshpsmreu  33906  lshpkrlem1  33907  lshpkrlem3  33909  pclfinN  34696  4atex  34872  dihglblem2N  36091  lcfl7N  36298  lcf1o  36348
  Copyright terms: Public domain W3C validator