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

Theorem cbvrexv 3069
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 1692 . 2  |-  F/ y
ph
2 nfv 1692 . 2  |-  F/ x ps
3 cbvralv.1 . 2  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
41, 2, 3cbvrex 3065 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 2792
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-ex 1598  df-nf 1602  df-sb 1725  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ral 2796  df-rex 2797
This theorem is referenced by:  cbvrex2v  3077  reu7  3278  reusv3  4641  xpdifid  5421  fliftfun  6191  grpridd  6496  funcnvuni  6734  fun11iun  6741  nneob  7299  pssnn  7736  frfi  7763  finsschain  7825  marypha1lem  7891  supmo  7910  suplub2  7919  ordtypelem3  7943  ordtypelem9  7949  wemaplem1  7969  brwdom3  8006  unwdomg  8008  cantnf  8110  cantnfOLD  8132  trcl  8157  infxpenc2  8397  infxpenc2OLD  8401  aceq2  8498  dfac5lem4  8505  kmlem9  8536  kmlem14  8541  fin23lem26  8703  fin1a2lem13  8790  axdc3lem3  8830  winainflem  9069  axgroth4  9208  suprlub  10506  supmul1  10509  supmullem1  10510  supmullem2  10511  supmul  10512  ublbneg  11170  zsupss  11175  xrsupsslem  11502  xrinfmsslem  11503  fsuppmapnn0fiub  12071  rexanre  13153  rexuzre  13159  rexico  13160  caurcvg2  13474  caucvgb  13476  summolem2  13512  summo  13513  mertens  13669  odd2np1lem  13917  gcdcllem1  14021  pceu  14242  4sqlem12  14346  vdwlem10  14380  vdwlem13  14383  vdwnn  14388  drsdirfi  15436  gaorb  16214  psgnunilem3  16390  psgnunilem4  16391  psgneu  16400  pj1eu  16583  efgsfo  16626  cyggeninv  16755  cygabl  16762  pgpfac1lem5  16998  pgpfac1  16999  pgpfaclem2  17001  lss1d  17477  lspsneq  17636  lspsolvlem  17656  lbsextlem2  17673  mplcoe5lem  17998  cygznlem3  18475  pmatcollpw3fi1lem2  19155  ordtrest2lem  19570  cnprest  19656  1stcfb  19812  1stcelcls  19828  elpt  19939  fbssfi  20204  fgcl  20245  rnelfmlem  20319  fmfnfmlem3  20323  txflf  20373  alexsubb  20412  alexsubALTlem4  20416  isucn2  20648  icccmplem2  21194  ply1divex  22403  coeeu  22488  plydivex  22558  aannenlem2  22590  ulmcau  22655  ulmbdd  22658  dchrptlem2  23405  bposlem9  23432  pntibndlem3  23642  pntlemi  23654  pntlemp  23660  pntleml  23661  pnt3  23662  legval  23836  legov  23837  legov2  23838  lnopp2hpgb  23997  erclwwlksym  24679  erclwwlktr  24680  erclwwlknsym  24691  erclwwlkntr  24692  eleclclwwlkn  24698  hashecclwwlkn1  24699  usghashecclwwlk  24700  frgraregorufr0  24917  isgrpo2  25064  grpoidinvlem3  25073  isgrp2d  25102  isgrpda  25164  ubthlem3  25653  norm1exi  26033  pjhthmo  26085  cdjreui  27216  cdj3i  27225  isarchi3  27597  archiabl  27608  ordtrest2NEWlem  27770  lmxrge0  27800  esumcvg  27958  eulerpartlems  28165  eulerpartlemgvv  28181  conpcon  28546  cvmlift2lem12  28625  cvmlift2lem13  28626  cvmlift3lem2  28631  cvmlift3lem7  28636  cvmlift3  28639  prodmolem2  29035  prodmo  29036  poseq  29301  soseq  29302  funtransport  29649  funray  29758  funline  29760  supaddc  30009  supadd  30010  ptrest  30016  ismblfin  30023  volsupnfl  30027  itg2addnclem  30034  fnessref  30143  neibastop2  30147  unirep  30171  filbcmb  30199  sdclem1  30204  sdc  30205  fdc  30206  incsequz  30209  heibor1lem  30273  heiborlem10  30284  isdrngo2  30329  prnc  30432  prtlem13  30577  prtlem15  30584  mzpcompact2lem  30652  eldioph3  30667  diophrex  30677  rexrabdioph  30695  eldioph4i  30714  aomclem8  30975  hbtlem2  31041  rngunsnply  31091  dvconstbi  31208  expgrowth  31209  limcperiod  31538  limsupre  31551  cncfshiftioo  31598  itgiccshift  31665  itgperiod  31666  fourierdlem42  31816  fourierdlem48  31822  fourierdlem81  31855  fourierdlem92  31866  fourierdlem96  31870  fourierdlem97  31871  fourierdlem98  31872  fourierdlem99  31873  fourierdlem105  31879  fourierdlem108  31882  fourierdlem110  31884  fourierdlem112  31886  fourierdlem113  31887  2zlidl  32440  2zrngamgm  32445  2zrngagrp  32449  2zrngmmgm  32452  lshpsmreu  34536  lshpkrlem1  34537  lshpkrlem3  34539  pclfinN  35326  4atex  35502  dihglblem2N  36723  lcfl7N  36930  lcf1o  36980
  Copyright terms: Public domain W3C validator