Theorem cbvrexv 3148

Description: Change the bound variable of a restricted existential quantifier using implicit substitution. (Contributed by NM, 2-Jun-1998.)

Hypothesis

Ref	Expression
cbvralv.1	⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
cbvrexv	⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓)

Distinct variable groups:   𝑥,𝐴   𝑦,𝐴   𝜑,𝑦   𝜓,𝑥

Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦)

Proof of Theorem cbvrexv

Step	Hyp	Ref	Expression
1		nfv 1830	. 2 ⊢ Ⅎ𝑦𝜑
2		nfv 1830	. 2 ⊢ Ⅎ𝑥𝜓
3		cbvralv.1	. 2 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
4	1, 2, 3	cbvrex 3144	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ↔ wb 195  ∃wrex 2897

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902

This theorem is referenced by:  cbvrex2v  3156  reu7  3368  reusv3  4802  xpdifid  5481  fliftfun  6462  grpridd  6772  funcnvuni  7012  fun11iun  7019  nneob  7619  pssnn  8063  frfi  8090  finsschain  8156  marypha1lem  8222  supmo  8241  suplub2  8250  infmo  8284  ordtypelem3  8308  ordtypelem9  8314  wemaplem1  8334  brwdom3  8370  unwdomg  8372  cantnf  8473  trcl  8487  infxpenc2  8728  aceq2  8825  dfac5lem4  8832  kmlem9  8863  kmlem14  8868  fin23lem26  9030  fin1a2lem13  9117  axdc3lem3  9157  winainflem  9394  axgroth4  9533  suprlub  10864  supaddc  10867  supadd  10868  supmul1  10869  supmullem1  10870  supmullem2  10871  supmul  10872  ublbneg  11649  zsupss  11653  xrsupsslem  12009  xrinfmsslem  12010  fsuppmapnn0fiubOLD  12653  rexanre  13934  rexuzre  13940  rexico  13941  caurcvg2  14256  caucvgb  14258  summolem2  14294  summo  14295  mertens  14457  prodmolem2  14504  prodmo  14505  odd2np1lem  14902  gcdcllem1  15059  pceu  15389  4sqlem12  15498  vdwlem10  15532  vdwlem13  15535  vdwnn  15540  drsdirfi  16761  dfgrp2  17270  dfgrp3lem  17336  gaorb  17563  psgnunilem3  17739  psgnunilem4  17740  psgneu  17749  pj1eu  17932  efgsfo  17975  cyggeninv  18108  cygabl  18115  pgpfac1lem5  18301  pgpfac1  18302  pgpfaclem2  18304  lss1d  18784  lspsneq  18943  lspsolvlem  18963  lbsextlem2  18980  mplcoe5lem  19288  cygznlem3  19737  pmatcollpw3fi1lem2  20411  ordtrest2lem  20817  cnprest  20903  1stcfb  21058  1stcelcls  21074  elpt  21185  fbssfi  21451  fgcl  21492  rnelfmlem  21566  fmfnfmlem3  21570  txflf  21620  alexsubb  21660  alexsubALTlem4  21664  isucn2  21893  icccmplem2  22434  ply1divex  23700  coeeu  23785  plydivex  23856  aannenlem2  23888  ulmcau  23953  ulmbdd  23956  dchrptlem2  24790  bposlem9  24817  2lgslem1b  24917  pntibndlem3  25081  pntlemi  25093  pntlemp  25099  pntleml  25100  pnt3  25101  legval  25279  legov  25280  legov2  25281  outpasch  25447  lnopp2hpgb  25455  colopp  25461  erclwwlksym  26342  erclwwlktr  26343  erclwwlknsym  26354  erclwwlkntr  26355  eleclclwwlkn  26360  hashecclwwlkn1  26361  usghashecclwwlk  26362  frgraregorufr0  26579  grpoidinvlem3  26744  ubthlem3  27112  norm1exi  27491  pjhthmo  27545  cdjreui  28675  cdj3i  28684  infxrge0glb  28920  isarchi3  29072  archiabl  29083  ordtrest2NEWlem  29296  lmxrge0  29326  esumcvg  29475  esum2d  29482  eulerpartlems  29749  eulerpartlemgvv  29765  conpcon  30471  cvmlift2lem12  30550  cvmlift2lem13  30551  cvmlift3lem2  30556  cvmlift3lem7  30561  cvmlift3  30564  poseq  30994  soseq  30995  funtransport  31308  funray  31417  funline  31419  fnessref  31522  neibastop2  31526  dissneqlem  32363  dissneq  32364  ptrest  32578  poimirlem27  32606  poimirlem32  32611  ismblfin  32620  volsupnfl  32624  itg2addnclem  32631  unirep  32677  filbcmb  32705  sdclem1  32709  sdc  32710  fdc  32711  incsequz  32714  heibor1lem  32778  heiborlem10  32789  isgrpda  32924  isdrngo2  32927  prnc  33036  prtlem13  33171  prtlem15  33178  lshpsmreu  33414  lshpkrlem1  33415  lshpkrlem3  33417  pclfinN  34204  4atex  34380  dihglblem2N  35601  lcfl7N  35808  lcf1o  35858  mzpcompact2lem  36332  eldioph3  36347  diophrex  36357  rexrabdioph  36376  eldioph4i  36394  aomclem8  36649  hbtlem2  36713  rngunsnply  36762  iunrelexpuztr  37030  ntrclsneine0lem  37382  dvconstbi  37555  expgrowth  37556  wessf1ornlem  38366  limcperiod  38695  limsupre  38708  cncfshiftioo  38778  itgiccshift  38872  itgperiod  38873  fourierdlem42  39042  fourierdlem48  39047  fourierdlem81  39080  fourierdlem92  39091  fourierdlem96  39095  fourierdlem97  39096  fourierdlem98  39097  fourierdlem99  39098  fourierdlem105  39104  fourierdlem108  39107  fourierdlem110  39109  fourierdlem112  39111  fourierdlem113  39112  hoidmvval0  39477  ovnhoi  39493  ovolval5lem3  39544  ovolval5  39545  fmtnofac2lem  40018  erclwwlkssym  41242  erclwwlkstr  41243  erclwwlksnsym  41254  erclwwlksntr  41255  eleclclwwlksn  41260  hashecclwwlksn1  41261  umgrhashecclwwlk  41262  frgrregorufr0  41489  2zlidl  41724  2zrngamgm  41729  2zrngagrp  41733  2zrngmmgm  41736