Theorem cbvrexvw 3241

Description: Change the bound variable of a restricted existential quantifier using implicit substitution. Version of cbvrexv 3352 with a disjoint variable condition, which does not require ax-10 2175, ax-11 2191, ax-12 2212, ax-13 2403. (Contributed by NM, 2-Jun-1998.) Avoid ax-13 2403. (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 2845	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvralvw.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	1, 2	anbi12d 641	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑦 ∈ 𝐴 ∧ 𝜓)))
4	3	cbvexvw 2057	. 2 ⊢ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ 𝜓))
5		df-rex 3087	. 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
6		df-rex 3087	. 2 ⊢ (∃𝑦 ∈ 𝐴 𝜓 ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ 𝜓))
7	4, 5, 6	3bitr4i 305	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399  ∃wex 1799   ∈ wcel 2142  ∃wrex 3086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-clel 2837  df-rex 3087

This theorem is referenced by:  cbvrex2vw  3245  reu7  3695  cbviunv  4996  disjiund  5091  reusv3  5362  xpdifid  6153  xpdifcnvepel  6154  fliftfun  7296  funcnvuni  7913  fiunlem  7923  poseq  8138  soseq  8139  nneob  8626  coflton  8641  cofon1  8642  cofon2  8643  pssnn  9137  frfi  9229  finsschain  9302  marypha1lem  9379  supmo  9398  suplub2  9407  infmo  9443  ordtypelem3  9468  ordtypelem9  9474  wemaplem1  9494  brwdom3  9530  unwdomg  9532  cantnf  9648  ttrcltr  9671  trcl  9683  infxpenc2  9978  aceq2  10075  dfac5lem4  10082  dfac5lem4OLD  10084  kmlem9  10115  kmlem14  10120  fin23lem26  10282  fin1a2lem13  10369  axdc3lem3  10409  winainflem  10651  axgroth4  10790  suprlub  12156  supaddc  12159  supadd  12160  supmul1  12161  supmullem1  12162  supmullem2  12163  supmul  12164  ublbneg  12934  zsupss  12938  xrsupsslem  13310  xrinfmsslem  13311  rexanre  15374  rexuzre  15380  rexico  15381  caurcvg2  15705  caucvgb  15707  summolem2  15743  summo  15744  mertens  15916  prodmolem2  15965  prodmo  15966  odd2np1lem  16374  gcdcllem1  16533  prmdvdsncoprmbd  16762  pceu  16882  4sqlem12  16992  vdwlem10  17026  vdwlem13  17029  vdwnn  17034  drsdirfi  18337  grprida  18709  smndex1mgm  18944  smndex1mndlem  18946  dfgrp2  19004  dfgrp3lem  19080  cyccom  19244  gaorb  19347  psgnunilem3  19536  psgnunilem4  19537  psgneu  19546  pj1eu  19736  efgsfo  19779  cyggeninv  19923  cygabl  19931  pgpfac1lem5  20121  pgpfac1  20122  pgpfaclem2  20124  lss1d  21027  lspsneq  21189  lspsolvlem  21209  lbsextlem2  21226  cygznlem3  21618  mplcoe5lem  22089  pmatcollpw3fi1lem2  22844  ordtrest2lem  23260  cnprest  23346  1stcfb  23502  1stcelcls  23518  elpt  23629  fbssfi  23894  fgcl  23935  rnelfmlem  24009  fmfnfmlem3  24013  txflf  24063  alexsubb  24103  alexsubALTlem4  24107  isucn2  24335  icccmplem2  24881  ply1divex  26194  coeeu  26282  plydivex  26358  aannenlem2  26390  ulmcau  26455  ulmbdd  26458  dchrptlem2  27326  bposlem9  27353  2lgslem1b  27453  pntibndlem3  27653  pntlemi  27665  pntlemp  27671  pntleml  27672  pnt3  27673  nosupprefixmo  27761  noinfprefixmo  27762  nosupcbv  27763  nosupdm  27765  nosupfv  27767  nosupres  27768  nosupbnd1lem1  27769  nosupbnd1lem4  27772  noinfcbv  27778  noinfdm  27780  noinfbnd1lem4  27787  cofslts  28008  coinitslts  28009  addsval2  28053  addcuts  28068  addsunif  28092  norecdiv  28280  recsne0  28282  bdayn0sf1o  28460  dfnns2  28462  n0seo  28511  pw2recs  28528  bdayfinbndcbv  28556  bdayfinbndlem1  28557  bdayfinbndlem2  28558  recut  28584  readdscl  28589  legval  28750  legov  28751  legov2  28752  outpasch  28925  lnopp2hpgb  28933  colopp  28939  elplngid  28986  lnincplng  28988  plngcp  28990  plngrot  28994  erclwwlksym  30220  erclwwlktr  30221  erclwwlknsym  30269  erclwwlkntr  30270  eleclclwwlkn  30275  hashecclwwlkn1  30276  umgrhashecclwwlk  30277  grpoidinvlem3  30706  ubthlem3  31072  norm1exi  31450  pjhthmo  31502  cdjreui  32632  cdj3i  32641  infxrge0glb  32964  mndlrinvb  33200  gsumwrd2dccatlem  33254  cyc3genpm  33329  isarchi3  33364  archiabl  33375  erler  33443  rlocisunit  33454  isdrng4  33479  1arithidomlem1  33728  1arithidom  33730  1arithufdlem2  33738  1arithufdlem3  33739  1arithufd  33741  fldext2chn  34022  constrconj  34039  constrextdg2lem  34042  constrextdg2  34043  constrfiss  34045  zarclsun  34164  ordtrest2NEWlem  34216  lmxrge0  34246  esumcvg  34380  esum2d  34387  eulerpartlems  34654  eulerpartlemgvv  34670  onvf1odlem2  35444  connpconn  35582  cvmlift2lem12  35661  cvmlift2lem13  35662  cvmlift3lem2  35667  cvmlift3lem7  35672  cvmlift3  35675  fmlasuc  35733  fmla1  35734  satffunlem1lem1  35749  satffunlem2lem1  35751  r1peuqusdeg1  35990  funtransport  36378  funray  36487  funline  36489  fnessref  36714  neibastop2  36718  dissneqlem  37831  dissneq  37832  pibt2  37908  ptrest  38115  poimirlem27  38143  poimirlem32  38148  ismblfin  38157  volsupnfl  38161  itg2addnclem  38167  unirep  38210  filbcmb  38236  sdclem1  38239  sdc  38240  fdc  38241  incsequz  38244  heibor1lem  38305  heiborlem10  38316  isgrpda  38451  isdrngo2  38454  prnc  38563  prtlem13  39489  prtlem15  39496  lshpsmreu  39730  lshpkrlem1  39731  lshpkrlem3  39733  pclfinN  40521  4atex  40697  dihglblem2N  41915  lcfl7N  42122  lcf1o  42172  supinf  42855  fimgmcyclem  43148  mzpcompact2lem  43329  eldioph3  43344  diophrex  43353  rexrabdioph  43368  eldioph4i  43386  aomclem8  43635  hbtlem2  43698  rngunsnply  43743  onsucrn  43845  iunrelexpuztr  44292  ntrclsneine0lem  44637  rexlimddvcbvw  44779  cpcoll2d  44832  mnuprdlem3  44847  dvconstbi  44907  expgrowth  44908  wessf1ornlem  45760  rnmptlb  45815  rnmptbdd  45817  rnmptbd2  45821  rnmptbd  45828  rexabsle  45990  uzub  46002  infrpgernmpt  46036  limcperiod  46201  limsupre  46212  limsupbnd1f  46257  climinf2  46278  climinfmpt  46286  limsupubuzmpt  46290  limsupmnf  46292  limsupre2  46296  limsupmnfuzlem  46297  limsupmnfuz  46298  limsupre2mpt  46301  limsupre3  46304  limsupre3mpt  46305  limsupre3uz  46307  limsupreuz  46308  limsupreuzmpt  46310  supcnvlimsup  46311  climuz  46315  lmbr3  46318  climrescn  46319  limsuplt2  46324  liminflelimsup  46347  limsupgt  46349  liminfreuz  46374  liminflt  46376  xlimpnfxnegmnf  46385  xlimmnf  46412  xlimpnf  46413  xlimmnfmpt  46414  xlimpnfmpt  46415  dfxlim2  46419  cncfshiftioo  46463  itgiccshift  46551  itgperiod  46552  fourierdlem42  46720  fourierdlem48  46725  fourierdlem81  46758  fourierdlem92  46769  fourierdlem96  46773  fourierdlem97  46774  fourierdlem98  46775  fourierdlem99  46776  fourierdlem105  46782  fourierdlem108  46785  fourierdlem110  46787  fourierdlem112  46789  fourierdlem113  46790  meaiunincf  47054  meaiuninc3v  47055  hoidmvval0  47158  ovnhoi  47174  ovolval5lem3  47225  ovolval5  47226  smfsup  47385  smfinflem  47388  smfinf  47389  nthrucw  47459  fsetsnfo  47644  2reuimp0  47705  nndivides2  47975  imaelsetpreimafv  47998  imasetpreimafvbijlemfo  48008  fundcmpsurinj  48012  fundcmpsurbijinj  48013  fmtnofac2lem  48174  2zlidl  48859  2zrngamgm  48864  2zrngagrp  48868  2zrngmmgm  48871  eenglngeehlnmlem1  49356  upciclem4  49787