Theorem cbvrexvw 3208

Description: Change the bound variable of a restricted existential quantifier using implicit substitution. Version of cbvrexv 3328 with a disjoint variable condition, which does not require ax-10 2142, ax-11 2158, ax-12 2178, ax-13 2370. (Contributed by NM, 2-Jun-1998.) Avoid ax-13 2370. (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 2811	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvralvw.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	1, 2	anbi12d 632	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑦 ∈ 𝐴 ∧ 𝜓)))
4	3	cbvexvw 2037	. 2 ⊢ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ 𝜓))
5		df-rex 3054	. 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
6		df-rex 3054	. 2 ⊢ (∃𝑦 ∈ 𝐴 𝜓 ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ 𝜓))
7	4, 5, 6	3bitr4i 303	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∃wex 1779   ∈ wcel 2109  ∃wrex 3053

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-clel 2803  df-rex 3054

This theorem is referenced by:  cbvrex2vw  3212  reu7  3692  cbviunv  4989  disjiund  5083  reusv3  5344  xpdifid  6117  fliftfun  7249  funcnvuni  7865  fiunlem  7877  poseq  8091  soseq  8092  nneob  8574  coflton  8589  cofon1  8590  cofon2  8591  pssnn  9082  frfi  9174  finsschain  9249  marypha1lem  9323  supmo  9342  suplub2  9351  infmo  9387  ordtypelem3  9412  ordtypelem9  9418  wemaplem1  9438  brwdom3  9474  unwdomg  9476  cantnf  9589  ttrcltr  9612  trcl  9624  infxpenc2  9916  aceq2  10013  dfac5lem4  10020  dfac5lem4OLD  10022  kmlem9  10053  kmlem14  10058  fin23lem26  10219  fin1a2lem13  10306  axdc3lem3  10346  winainflem  10587  axgroth4  10726  suprlub  12089  supaddc  12092  supadd  12093  supmul1  12094  supmullem1  12095  supmullem2  12096  supmul  12097  ublbneg  12834  zsupss  12838  xrsupsslem  13209  xrinfmsslem  13210  rexanre  15254  rexuzre  15260  rexico  15261  caurcvg2  15585  caucvgb  15587  summolem2  15623  summo  15624  mertens  15793  prodmolem2  15842  prodmo  15843  odd2np1lem  16251  gcdcllem1  16410  prmdvdsncoprmbd  16638  pceu  16758  4sqlem12  16868  vdwlem10  16902  vdwlem13  16905  vdwnn  16910  drsdirfi  18211  grprida  18549  smndex1mgm  18781  smndex1mndlem  18783  dfgrp2  18841  dfgrp3lem  18917  cyccom  19082  gaorb  19186  psgnunilem3  19375  psgnunilem4  19376  psgneu  19385  pj1eu  19575  efgsfo  19618  cyggeninv  19762  cygabl  19770  pgpfac1lem5  19960  pgpfac1  19961  pgpfaclem2  19963  lss1d  20866  lspsneq  21029  lspsolvlem  21049  lbsextlem2  21066  cygznlem3  21476  mplcoe5lem  21944  pmatcollpw3fi1lem2  22672  ordtrest2lem  23088  cnprest  23174  1stcfb  23330  1stcelcls  23346  elpt  23457  fbssfi  23722  fgcl  23763  rnelfmlem  23837  fmfnfmlem3  23841  txflf  23891  alexsubb  23931  alexsubALTlem4  23935  isucn2  24164  icccmplem2  24710  ply1divex  26040  coeeu  26128  plydivex  26203  aannenlem2  26235  ulmcau  26302  ulmbdd  26305  dchrptlem2  27174  bposlem9  27201  2lgslem1b  27301  pntibndlem3  27501  pntlemi  27513  pntlemp  27519  pntleml  27520  pnt3  27521  nosupprefixmo  27610  noinfprefixmo  27611  nosupcbv  27612  nosupdm  27614  nosupfv  27616  nosupres  27617  nosupbnd1lem1  27618  nosupbnd1lem4  27621  noinfcbv  27627  noinfdm  27629  noinfbnd1lem4  27636  cofsslt  27831  coinitsslt  27832  addsval2  27875  addscut  27890  addsunif  27914  norecdiv  28098  recsne0  28100  bdayn0sf1o  28264  dfnns2  28266  n0seo  28313  pw2recs  28330  recut  28365  readdscl  28368  legval  28529  legov  28530  legov2  28531  outpasch  28700  lnopp2hpgb  28708  colopp  28714  erclwwlksym  29965  erclwwlktr  29966  erclwwlknsym  30014  erclwwlkntr  30015  eleclclwwlkn  30020  hashecclwwlkn1  30021  umgrhashecclwwlk  30022  grpoidinvlem3  30450  ubthlem3  30816  norm1exi  31194  pjhthmo  31246  cdjreui  32376  cdj3i  32385  infxrge0glb  32708  mndlrinvb  32979  gsumwrd2dccatlem  33019  cyc3genpm  33094  isarchi3  33129  archiabl  33140  erler  33205  isdrng4  33234  1arithidomlem1  33472  1arithidom  33474  1arithufdlem2  33482  1arithufdlem3  33483  1arithufd  33485  fldext2chn  33695  constrconj  33712  constrextdg2lem  33715  constrextdg2  33716  constrfiss  33718  zarclsun  33837  ordtrest2NEWlem  33889  lmxrge0  33919  esumcvg  34053  esum2d  34060  eulerpartlems  34328  eulerpartlemgvv  34344  onvf1odlem2  35077  connpconn  35208  cvmlift2lem12  35287  cvmlift2lem13  35288  cvmlift3lem2  35293  cvmlift3lem7  35298  cvmlift3  35301  fmlasuc  35359  fmla1  35360  satffunlem1lem1  35375  satffunlem2lem1  35377  r1peuqusdeg1  35616  funtransport  36005  funray  36114  funline  36116  fnessref  36331  neibastop2  36335  dissneqlem  37314  dissneq  37315  pibt2  37391  ptrest  37599  poimirlem27  37627  poimirlem32  37632  ismblfin  37641  volsupnfl  37645  itg2addnclem  37651  unirep  37694  filbcmb  37720  sdclem1  37723  sdc  37724  fdc  37725  incsequz  37728  heibor1lem  37789  heiborlem10  37800  isgrpda  37935  isdrngo2  37938  prnc  38047  prtlem13  38847  prtlem15  38854  lshpsmreu  39088  lshpkrlem1  39089  lshpkrlem3  39091  pclfinN  39879  4atex  40055  dihglblem2N  41273  lcfl7N  41480  lcf1o  41530  supinf  42215  fimgmcyclem  42506  mzpcompact2lem  42724  eldioph3  42739  diophrex  42748  rexrabdioph  42767  eldioph4i  42785  aomclem8  43034  hbtlem2  43097  rngunsnply  43142  onsucrn  43244  iunrelexpuztr  43692  ntrclsneine0lem  44037  rexlimddvcbvw  44179  cpcoll2d  44232  mnuprdlem3  44247  dvconstbi  44307  expgrowth  44308  wessf1ornlem  45163  rnmptlb  45221  rnmptbdd  45223  rnmptbd2  45227  rnmptbd  45234  rexabsle  45398  uzub  45410  infrpgernmpt  45444  limcperiod  45609  limsupre  45622  limsupbnd1f  45667  climinf2  45688  climinfmpt  45696  limsupubuzmpt  45700  limsupmnf  45702  limsupre2  45706  limsupmnfuzlem  45707  limsupmnfuz  45708  limsupre2mpt  45711  limsupre3  45714  limsupre3mpt  45715  limsupre3uz  45717  limsupreuz  45718  limsupreuzmpt  45720  supcnvlimsup  45721  climuz  45725  lmbr3  45728  climrescn  45729  limsuplt2  45734  liminflelimsup  45757  limsupgt  45759  liminfreuz  45784  liminflt  45786  xlimpnfxnegmnf  45795  xlimmnf  45822  xlimpnf  45823  xlimmnfmpt  45824  xlimpnfmpt  45825  dfxlim2  45829  cncfshiftioo  45873  itgiccshift  45961  itgperiod  45962  fourierdlem42  46130  fourierdlem48  46135  fourierdlem81  46168  fourierdlem92  46179  fourierdlem96  46183  fourierdlem97  46184  fourierdlem98  46185  fourierdlem99  46186  fourierdlem105  46192  fourierdlem108  46195  fourierdlem110  46197  fourierdlem112  46199  fourierdlem113  46200  meaiunincf  46464  meaiuninc3v  46465  hoidmvval0  46568  ovnhoi  46584  ovolval5lem3  46635  ovolval5  46636  smfsup  46795  smfinflem  46798  smfinf  46799  fsetsnfo  47037  2reuimp0  47098  imaelsetpreimafv  47379  imasetpreimafvbijlemfo  47389  fundcmpsurinj  47393  fundcmpsurbijinj  47394  fmtnofac2lem  47552  2zlidl  48224  2zrngamgm  48229  2zrngagrp  48233  2zrngmmgm  48236  eenglngeehlnmlem1  48722  upciclem4  49154