Theorem cbvrexvw 3250

Description: Change the bound variable of a restricted existential quantifier using implicit substitution. Version of cbvrexv 3361 with a disjoint variable condition, which does not require ax-10 2182, ax-11 2198, ax-12 2219, ax-13 2410. (Contributed by NM, 2-Jun-1998.) Avoid ax-13 2410. (Revised by GG, 10-Jan-2024.)

Hypothesis

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

Assertion

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

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

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

Proof of Theorem cbvrexvw

Step	Hyp	Ref	Expression
1		eleq1w 2852	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvralvw.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	1, 2	anbi12d 643	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑦 ∈ 𝐴 ∧ 𝜓)))
4	3	cbvexvw 2064	. 2 ⊢ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ 𝜓))
5		df-rex 3096	. 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
6		df-rex 3096	. 2 ⊢ (∃𝑦 ∈ 𝐴 𝜓 ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ 𝜓))
7	4, 5, 6	3bitr4i 306	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400  ∃wex 1806   ∈ wcel 2149  ∃wrex 3095

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-clel 2844  df-rex 3096

This theorem is referenced by:  cbvrex2vw  3254  reu7  3704  cbviunv  5007  disjiund  5104  reusv3  5377  xpdifid  6166  xpdifcnvepel  6167  fliftfun  7311  funcnvuni  7928  fiunlem  7938  poseq  8153  soseq  8154  nneob  8641  coflton  8656  cofon1  8657  cofon2  8658  pssnn  9152  frfi  9244  finsschain  9315  marypha1lem  9392  supmo  9411  suplub2  9420  infmo  9456  ordtypelem3  9481  ordtypelem9  9487  wemaplem1  9507  brwdom3  9543  unwdomg  9545  cantnf  9661  ttrcltr  9684  trcl  9696  infxpenc2  10005  aceq2  10102  dfac5lem4  10109  kmlem9  10141  kmlem14  10146  fin23lem26  10308  fin1a2lem13  10395  axdc3lem3  10435  winainflem  10677  axgroth4  10816  suprlub  12178  supaddc  12181  supadd  12182  supmul1  12183  supmullem1  12184  supmullem2  12185  supmul  12186  ublbneg  12956  zsupss  12960  xrsupsslem  13332  xrinfmsslem  13333  rexanre  15397  rexuzre  15403  rexico  15404  caurcvg2  15728  caucvgb  15730  summolem2  15766  summo  15767  mertens  15939  prodmolem2  15988  prodmo  15989  odd2np1lem  16397  gcdcllem1  16556  prmdvdsncoprmbd  16785  pceu  16905  4sqlem12  17015  vdwlem10  17049  vdwlem13  17052  vdwnn  17057  drsdirfi  18360  grprida  18732  smndex1mgm  18968  smndex1mndlem  18970  dfgrp2  19028  dfgrp3lem  19103  cyccom  19273  gaorb  19376  psgnunilem3  19565  psgnunilem4  19566  psgneu  19575  pj1eu  19765  efgsfo  19808  cyggeninv  19952  cygabl  19960  pgpfac1lem5  20150  pgpfac1  20151  pgpfaclem2  20153  lss1d  21061  lspsneq  21223  lspsolvlem  21243  lbsextlem2  21260  cygznlem3  21687  mplcoe5lem  22158  pmatcollpw3fi1lem2  22912  ordtrest2lem  23328  cnprest  23414  1stcfb  23570  1stcelcls  23586  elpt  23697  fbssfi  23962  fgcl  24003  rnelfmlem  24077  fmfnfmlem3  24081  txflf  24131  alexsubb  24171  alexsubALTlem4  24175  isucn2  24403  icccmplem2  24949  ply1divex  26262  coeeu  26350  plydivex  26426  aannenlem2  26458  ulmcau  26523  ulmbdd  26526  dchrptlem2  27394  bposlem9  27421  2lgslem1b  27521  pntibndlem3  27721  pntlemi  27733  pntlemp  27739  pntleml  27740  pnt3  27741  nosupprefixmo  27829  noinfprefixmo  27830  nosupcbv  27831  nosupdm  27833  nosupfv  27835  nosupres  27836  nosupbnd1lem1  27837  nosupbnd1lem4  27840  noinfcbv  27846  noinfdm  27848  noinfbnd1lem4  27855  cofslts  28076  coinitslts  28077  addsval2  28121  addcuts  28136  addsunif  28160  norecdiv  28348  recsne0  28350  bdayn0sf1o  28528  dfnns2  28530  n0seo  28579  pw2recs  28596  bdayfinbndcbv  28624  bdayfinbndlem1  28625  bdayfinbndlem2  28626  recut  28652  readdscl  28657  legval  28818  legov  28819  legov2  28820  outpasch  28995  lnopp2hpgb  29003  colopp  29009  elplngid  29021  lnincplng  29023  plngcp  29025  plngrot  29029  nhpmirhp  29037  lnperpexs  29070  ragraghl  29103  prlnghpg  29150  prlngmo  29156  erclwwlksym  30312  erclwwlktr  30313  erclwwlknsym  30361  erclwwlkntr  30362  eleclclwwlkn  30367  hashecclwwlkn1  30368  umgrhashecclwwlk  30369  grpoidinvlem3  30798  ubthlem3  31164  norm1exi  31542  pjhthmo  31594  cdjreui  32724  cdj3i  32733  infxrge0glb  33050  mndlrinvb  33285  gsumwrd2dccatlem  33337  cyc3genpm  33412  isarchi3  33447  archiabl  33458  erler  33525  rlocisunit  33536  isdrng4  33558  1arithidomlem1  33769  1arithidom  33771  1arithufdlem2  33779  1arithufdlem3  33780  1arithufd  33782  fldext2chn  34062  constrconj  34079  constrextdg2lem  34082  constrextdg2  34083  constrfiss  34085  zarclsun  34204  ordtrest2NEWlem  34256  lmxrge0  34286  esumcvg  34420  esum2d  34427  eulerpartlems  34694  eulerpartlemgvv  34710  onvf1odlem2  35486  connpconn  35625  cvmlift2lem12  35704  cvmlift2lem13  35705  cvmlift3lem2  35710  cvmlift3lem7  35715  cvmlift3  35718  fmlasuc  35776  fmla1  35777  satffunlem1lem1  35792  satffunlem2lem1  35794  r1peuqusdeg1  36033  funtransport  36421  funray  36530  funline  36532  fnessref  36756  neibastop2  36760  dissneqlem  37873  dissneq  37874  pibt2  37950  ptrest  38157  poimirlem27  38185  poimirlem32  38190  ismblfin  38199  volsupnfl  38203  itg2addnclem  38209  unirep  38252  filbcmb  38278  sdclem1  38281  sdc  38282  fdc  38283  incsequz  38286  heibor1lem  38347  heiborlem10  38358  isgrpda  38493  isdrngo2  38496  prnc  38605  prtlem13  39531  prtlem15  39538  lshpsmreu  39772  lshpkrlem1  39773  lshpkrlem3  39775  pclfinN  40563  4atex  40739  dihglblem2N  41957  lcfl7N  42164  lcf1o  42214  supinf  42899  fimgmcyclem  43192  mzpcompact2lem  43373  eldioph3  43388  diophrex  43397  rexrabdioph  43412  eldioph4i  43430  aomclem8  43679  hbtlem2  43742  rngunsnply  43787  onsucrn  43889  iunrelexpuztr  44336  ntrclsneine0lem  44681  rexlimddvcbvw  44821  cpcoll2d  44860  mnuprdlem3  44875  dvconstbi  44935  expgrowth  44936  wessf1ornlem  45794  rnmptlb  45849  rnmptbdd  45851  rnmptbd2  45855  rnmptbd  45862  rexabsle  46024  uzub  46036  infrpgernmpt  46070  limcperiod  46235  limsupre  46246  limsupbnd1f  46291  climinf2  46312  climinfmpt  46320  limsupubuzmpt  46324  limsupmnf  46326  limsupre2  46330  limsupmnfuzlem  46331  limsupmnfuz  46332  limsupre2mpt  46335  limsupre3  46338  limsupre3mpt  46339  limsupre3uz  46341  limsupreuz  46342  limsupreuzmpt  46344  supcnvlimsup  46345  climuz  46349  lmbr3  46352  climrescn  46353  limsuplt2  46358  liminflelimsup  46381  limsupgt  46383  liminfreuz  46408  liminflt  46410  xlimpnfxnegmnf  46419  xlimmnf  46446  xlimpnf  46447  xlimmnfmpt  46448  xlimpnfmpt  46449  dfxlim2  46453  cncfshiftioo  46497  itgiccshift  46585  itgperiod  46586  fourierdlem42  46754  fourierdlem48  46759  fourierdlem81  46792  fourierdlem92  46803  fourierdlem96  46807  fourierdlem97  46808  fourierdlem98  46809  fourierdlem99  46810  fourierdlem105  46816  fourierdlem108  46819  fourierdlem110  46821  fourierdlem112  46823  fourierdlem113  46824  meaiunincf  47088  meaiuninc3v  47089  hoidmvval0  47192  ovnhoi  47208  ovolval5lem3  47259  ovolval5  47260  smfsup  47419  smfinflem  47422  smfinf  47423  nthrucw  47493  fsetsnfo  47678  2reuimp0  47739  nndivides2  48009  imaelsetpreimafv  48032  imasetpreimafvbijlemfo  48042  fundcmpsurinj  48046  fundcmpsurbijinj  48047  fmtnofac2lem  48208  2zlidl  48893  2zrngamgm  48898  2zrngagrp  48902  2zrngmmgm  48905  eenglngeehlnmlem1  49401  upciclem4  49831