Theorem cbvrexv 3172

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

Step	Hyp	Ref	Expression
1		nfv 1843	. 2 |- F/ y ph
2		nfv 1843	. 2 |- F/ x ps
3		cbvralv.1	. 2 |- ( x = y -> ( ph <-> ps ) )
4	1, 2, 3	cbvrex 3168	1 |- ( E. x e. A ph <-> E. y e. A ps )

Syntax hints:   -> wi 4   <-> wb 196   E.wrex 2913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918

This theorem is referenced by:  cbvrex2v  3180  reu7  3401  disjiund  4643  reusv3  4876  xpdifid  5562  fliftfun  6562  grpridd  6874  funcnvuni  7119  fun11iun  7126  nneob  7732  pssnn  8178  frfi  8205  finsschain  8273  marypha1lem  8339  supmo  8358  suplub2  8367  infmo  8401  ordtypelem3  8425  ordtypelem9  8431  wemaplem1  8451  brwdom3  8487  unwdomg  8489  cantnf  8590  trcl  8604  infxpenc2  8845  aceq2  8942  dfac5lem4  8949  kmlem9  8980  kmlem14  8985  fin23lem26  9147  fin1a2lem13  9234  axdc3lem3  9274  winainflem  9515  axgroth4  9654  suprlub  10987  supaddc  10990  supadd  10991  supmul1  10992  supmullem1  10993  supmullem2  10994  supmul  10995  ublbneg  11773  zsupss  11777  xrsupsslem  12137  xrinfmsslem  12138  fsuppmapnn0fiubOLD  12791  rexanre  14086  rexuzre  14092  rexico  14093  caurcvg2  14408  caucvgb  14410  summolem2  14447  summo  14448  mertens  14618  prodmolem2  14665  prodmo  14666  odd2np1lem  15064  gcdcllem1  15221  pceu  15551  4sqlem12  15660  vdwlem10  15694  vdwlem13  15697  vdwnn  15702  drsdirfi  16938  dfgrp2  17447  dfgrp3lem  17513  gaorb  17740  psgnunilem3  17916  psgnunilem4  17917  psgneu  17926  pj1eu  18109  efgsfo  18152  cyggeninv  18285  cygabl  18292  pgpfac1lem5  18478  pgpfac1  18479  pgpfaclem2  18481  lss1d  18963  lspsneq  19122  lspsolvlem  19142  lbsextlem2  19159  mplcoe5lem  19467  cygznlem3  19918  pmatcollpw3fi1lem2  20592  ordtrest2lem  21007  cnprest  21093  1stcfb  21248  1stcelcls  21264  elpt  21375  fbssfi  21641  fgcl  21682  rnelfmlem  21756  fmfnfmlem3  21760  txflf  21810  alexsubb  21850  alexsubALTlem4  21854  isucn2  22083  icccmplem2  22626  ply1divex  23896  coeeu  23981  plydivex  24052  aannenlem2  24084  ulmcau  24149  ulmbdd  24152  dchrptlem2  24990  bposlem9  25017  2lgslem1b  25117  pntibndlem3  25281  pntlemi  25293  pntlemp  25299  pntleml  25300  pnt3  25301  legval  25479  legov  25480  legov2  25481  outpasch  25647  lnopp2hpgb  25655  colopp  25661  erclwwlkssym  26935  erclwwlkstr  26936  erclwwlksnsym  26947  erclwwlksntr  26948  eleclclwwlksn  26953  hashecclwwlksn1  26954  umgrhashecclwwlk  26955  grpoidinvlem3  27360  ubthlem3  27728  norm1exi  28107  pjhthmo  28161  cdjreui  29291  cdj3i  29300  infxrge0glb  29530  isarchi3  29741  archiabl  29752  ordtrest2NEWlem  29968  lmxrge0  29998  esumcvg  30148  esum2d  30155  eulerpartlems  30422  eulerpartlemgvv  30438  connpconn  31217  cvmlift2lem12  31296  cvmlift2lem13  31297  cvmlift3lem2  31302  cvmlift3lem7  31307  cvmlift3  31310  poseq  31750  soseq  31751  noprefixmo  31848  nosupdm  31850  nosupfv  31852  nosupres  31853  nosupbnd1lem1  31854  nosupbnd1lem4  31857  funtransport  32138  funray  32247  funline  32249  fnessref  32352  neibastop2  32356  dissneqlem  33187  dissneq  33188  ptrest  33408  poimirlem27  33436  poimirlem32  33441  ismblfin  33450  volsupnfl  33454  itg2addnclem  33461  unirep  33507  filbcmb  33535  sdclem1  33539  sdc  33540  fdc  33541  incsequz  33544  heibor1lem  33608  heiborlem10  33619  isgrpda  33754  isdrngo2  33757  prnc  33866  prtlem13  34153  prtlem15  34160  lshpsmreu  34396  lshpkrlem1  34397  lshpkrlem3  34399  pclfinN  35186  4atex  35362  dihglblem2N  36583  lcfl7N  36790  lcf1o  36840  mzpcompact2lem  37314  eldioph3  37329  diophrex  37339  rexrabdioph  37358  eldioph4i  37376  aomclem8  37631  hbtlem2  37694  rngunsnply  37743  iunrelexpuztr  38011  ntrclsneine0lem  38362  dvconstbi  38533  expgrowth  38534  wessf1ornlem  39371  rnmptlb  39453  rnmptbdd  39456  rnmptbd2  39464  rnmptbd  39471  rexabsle  39646  uzub  39658  infrpgernmpt  39695  limcperiod  39860  limsupre  39873  limsupref  39917  limsupbnd1f  39918  climinfmpt  39947  limsupubuzmpt  39951  limsupmnf  39953  limsupre2  39957  limsupmnfuzlem  39958  limsupmnfuz  39959  limsupre2mpt  39962  limsupre3  39965  limsupre3mpt  39966  limsupre3uz  39968  limsupreuz  39969  limsupreuzmpt  39971  supcnvlimsup  39972  climuz  39976  lmbr3  39979  climrescn  39980  limsuplt2  39985  liminflelimsup  40008  limsupgt  40010  liminfreuz  40035  liminflt  40037  xlimmnf  40067  xlimpnf  40068  xlimmnfmpt  40069  xlimpnfmpt  40070  dfxlim2  40074  cncfshiftioo  40105  itgiccshift  40196  itgperiod  40197  fourierdlem42  40366  fourierdlem48  40371  fourierdlem81  40404  fourierdlem92  40415  fourierdlem96  40419  fourierdlem97  40420  fourierdlem98  40421  fourierdlem99  40422  fourierdlem105  40428  fourierdlem108  40431  fourierdlem110  40433  fourierdlem112  40435  fourierdlem113  40436  hoidmvval0  40801  ovnhoi  40817  ovolval5lem3  40868  ovolval5  40869  smfsup  41020  smfinflem  41023  smfinf  41024  fmtnofac2lem  41480  2zlidl  41934  2zrngamgm  41939  2zrngagrp  41943  2zrngmmgm  41946