Theorem cbvrexvw 3236

Description: Change the bound variable of a restricted existential quantifier using implicit substitution. Version of cbvrexv 3362 with a disjoint variable condition, which does not require ax-10 2138, ax-11 2155, ax-12 2172, ax-13 2372. (Contributed by NM, 2-Jun-1998.) Avoid ax-13 2372. (Revised by Gino Giotto, 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 2817	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvralvw.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	1, 2	anbi12d 632	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑦 ∈ 𝐴 ∧ 𝜓)))
4	3	cbvexvw 2041	. 2 ⊢ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ 𝜓))
5		df-rex 3072	. 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
6		df-rex 3072	. 2 ⊢ (∃𝑦 ∈ 𝐴 𝜓 ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ 𝜓))
7	4, 5, 6	3bitr4i 303	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397  ∃wex 1782   ∈ wcel 2107  ∃wrex 3071

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-clel 2811  df-rex 3072

This theorem is referenced by:  cbvrex2vw  3240  reu7  3729  disjiund  5139  reusv3  5404  xpdifid  6168  fliftfun  7309  funcnvuni  7922  fiunlem  7928  poseq  8144  soseq  8145  nneob  8655  coflton  8670  cofon1  8671  cofon2  8672  pssnn  9168  pssnnOLD  9265  frfi  9288  finsschain  9359  marypha1lem  9428  supmo  9447  suplub2  9456  infmo  9490  ordtypelem3  9515  ordtypelem9  9521  wemaplem1  9541  brwdom3  9577  unwdomg  9579  cantnf  9688  ttrcltr  9711  trcl  9723  infxpenc2  10017  aceq2  10114  dfac5lem4  10121  kmlem9  10153  kmlem14  10158  fin23lem26  10320  fin1a2lem13  10407  axdc3lem3  10447  winainflem  10688  axgroth4  10827  suprlub  12178  supaddc  12181  supadd  12182  supmul1  12183  supmullem1  12184  supmullem2  12185  supmul  12186  ublbneg  12917  zsupss  12921  xrsupsslem  13286  xrinfmsslem  13287  rexanre  15293  rexuzre  15299  rexico  15300  caurcvg2  15624  caucvgb  15626  summolem2  15662  summo  15663  mertens  15832  prodmolem2  15879  prodmo  15880  odd2np1lem  16283  gcdcllem1  16440  prmdvdsncoprmbd  16663  pceu  16779  4sqlem12  16889  vdwlem10  16923  vdwlem13  16926  vdwnn  16931  drsdirfi  18258  grprida  18594  smndex1mgm  18788  smndex1mndlem  18790  dfgrp2  18847  dfgrp3lem  18921  cyccom  19080  gaorb  19171  psgnunilem3  19364  psgnunilem4  19365  psgneu  19374  pj1eu  19564  efgsfo  19607  cyggeninv  19751  cygabl  19759  pgpfac1lem5  19949  pgpfac1  19950  pgpfaclem2  19952  lss1d  20574  lspsneq  20735  lspsolvlem  20755  lbsextlem2  20772  cygznlem3  21125  mplcoe5lem  21594  pmatcollpw3fi1lem2  22289  ordtrest2lem  22707  cnprest  22793  1stcfb  22949  1stcelcls  22965  elpt  23076  fbssfi  23341  fgcl  23382  rnelfmlem  23456  fmfnfmlem3  23460  txflf  23510  alexsubb  23550  alexsubALTlem4  23554  isucn2  23784  icccmplem2  24339  ply1divex  25654  coeeu  25739  plydivex  25810  aannenlem2  25842  ulmcau  25907  ulmbdd  25910  dchrptlem2  26768  bposlem9  26795  2lgslem1b  26895  pntibndlem3  27095  pntlemi  27107  pntlemp  27113  pntleml  27114  pnt3  27115  nosupprefixmo  27203  noinfprefixmo  27204  nosupcbv  27205  nosupdm  27207  nosupfv  27209  nosupres  27210  nosupbnd1lem1  27211  nosupbnd1lem4  27214  noinfcbv  27220  noinfdm  27222  noinfbnd1lem4  27229  cofsslt  27405  coinitsslt  27406  addsval2  27447  addscut  27462  addsunif  27485  norecdiv  27638  legval  27835  legov  27836  legov2  27837  outpasch  28006  lnopp2hpgb  28014  colopp  28020  erclwwlksym  29274  erclwwlktr  29275  erclwwlknsym  29323  erclwwlkntr  29324  eleclclwwlkn  29329  hashecclwwlkn1  29330  umgrhashecclwwlk  29331  grpoidinvlem3  29759  ubthlem3  30125  norm1exi  30503  pjhthmo  30555  cdjreui  31685  cdj3i  31694  infxrge0glb  31978  cyc3genpm  32311  isarchi3  32333  archiabl  32344  isdrng4  32395  zarclsun  32850  ordtrest2NEWlem  32902  lmxrge0  32932  esumcvg  33084  esum2d  33091  eulerpartlems  33359  eulerpartlemgvv  33375  connpconn  34226  cvmlift2lem12  34305  cvmlift2lem13  34306  cvmlift3lem2  34311  cvmlift3lem7  34316  cvmlift3  34319  fmlasuc  34377  fmla1  34378  satffunlem1lem1  34393  satffunlem2lem1  34395  funtransport  35003  funray  35112  funline  35114  fnessref  35242  neibastop2  35246  dissneqlem  36221  dissneq  36222  pibt2  36298  ptrest  36487  poimirlem27  36515  poimirlem32  36520  ismblfin  36529  volsupnfl  36533  itg2addnclem  36539  unirep  36582  filbcmb  36608  sdclem1  36611  sdc  36612  fdc  36613  incsequz  36616  heibor1lem  36677  heiborlem10  36688  isgrpda  36823  isdrngo2  36826  prnc  36935  prtlem13  37738  prtlem15  37745  lshpsmreu  37979  lshpkrlem1  37980  lshpkrlem3  37982  pclfinN  38771  4atex  38947  dihglblem2N  40165  lcfl7N  40372  lcf1o  40422  mzpcompact2lem  41489  eldioph3  41504  diophrex  41513  rexrabdioph  41532  eldioph4i  41550  aomclem8  41803  hbtlem2  41866  rngunsnply  41915  onsucrn  42021  iunrelexpuztr  42470  ntrclsneine0lem  42815  rexlimddvcbvw  42958  cpcoll2d  43018  mnuprdlem3  43033  dvconstbi  43093  expgrowth  43094  wessf1ornlem  43882  rnmptlb  43947  rnmptbdd  43949  rnmptbd2  43953  rnmptbd  43960  rexabsle  44129  uzub  44141  infrpgernmpt  44175  limcperiod  44344  limsupre  44357  limsupbnd1f  44402  climinf2  44423  climinfmpt  44431  limsupubuzmpt  44435  limsupmnf  44437  limsupre2  44441  limsupmnfuzlem  44442  limsupmnfuz  44443  limsupre2mpt  44446  limsupre3  44449  limsupre3mpt  44450  limsupre3uz  44452  limsupreuz  44453  limsupreuzmpt  44455  supcnvlimsup  44456  climuz  44460  lmbr3  44463  climrescn  44464  limsuplt2  44469  liminflelimsup  44492  limsupgt  44494  liminfreuz  44519  liminflt  44521  xlimpnfxnegmnf  44530  xlimmnf  44557  xlimpnf  44558  xlimmnfmpt  44559  xlimpnfmpt  44560  dfxlim2  44564  cncfshiftioo  44608  itgiccshift  44696  itgperiod  44697  fourierdlem42  44865  fourierdlem48  44870  fourierdlem81  44903  fourierdlem92  44914  fourierdlem96  44918  fourierdlem97  44919  fourierdlem98  44920  fourierdlem99  44921  fourierdlem105  44927  fourierdlem108  44930  fourierdlem110  44932  fourierdlem112  44934  fourierdlem113  44935  meaiunincf  45199  meaiuninc3v  45200  hoidmvval0  45303  ovnhoi  45319  ovolval5lem3  45370  ovolval5  45371  smfsup  45530  smfinflem  45533  smfinf  45534  fsetsnfo  45763  2reuimp0  45822  imaelsetpreimafv  46063  imasetpreimafvbijlemfo  46073  fundcmpsurinj  46077  fundcmpsurbijinj  46078  fmtnofac2lem  46236  2zlidl  46832  2zrngamgm  46837  2zrngagrp  46841  2zrngmmgm  46844  eenglngeehlnmlem1  47423