Theorem cbvrexvw 3246

Description: Change the bound variable of a restricted existential quantifier using implicit substitution. Version of cbvrexv 3356 with a disjoint variable condition, which does not require ax-10 2179, ax-11 2195, ax-12 2216, ax-13 2406. (Contributed by NM, 2-Jun-1998.) Avoid ax-13 2406. (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 2848	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvralvw.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	1, 2	anbi12d 644	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑦 ∈ 𝐴 ∧ 𝜓)))
4	3	cbvexvw 2070	. 2 ⊢ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ 𝜓))
5		df-rex 3092	. 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
6		df-rex 3092	. 2 ⊢ (∃𝑦 ∈ 𝐴 𝜓 ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ 𝜓))
7	4, 5, 6	3bitr4i 306	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401  ∃wex 1812   ∈ wcel 2146  ∃wrex 3091

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-clel 2840  df-rex 3092

This theorem is used by:  cbvrex2vw  3250  reu7  3697  cbviunv  5005  disjiund  5102  reusv3  5378  xpdifid  6167  xpdifcnvepel  6168  fliftfun  7319  funcnvuni  7935  fiunlem  7945  poseq  8160  soseq  8161  nneob  8648  coflton  8663  cofon1  8664  cofon2  8665  pssnn  9160  frfi  9252  finsschain  9323  marypha1lem  9400  supmo  9419  suplub2  9428  infmo  9464  ordtypelem3  9489  ordtypelem9  9495  wemaplem1  9515  brwdom3  9551  unwdomg  9553  cantnf  9669  ttrcltr  9692  trcl  9704  infxpenc2  10022  aceq2  10119  dfac5lem4  10126  kmlem9  10158  kmlem14  10163  fin23lem26  10324  fin1a2lem13  10411  axdc3lem3  10451  winainflem  10693  axgroth4  10832  suprlub  12194  supaddc  12197  supadd  12198  supmul1  12199  supmullem1  12200  supmullem2  12201  supmul  12202  ublbneg  12973  zsupss  12977  xrsupsslem  13349  xrinfmsslem  13350  rexanre  15422  rexuzre  15428  rexico  15429  caurcvg2  15753  caucvgb  15755  summolem2  15790  summo  15791  mertens  15963  prodmolem2  16012  prodmo  16013  odd2np1lem  16420  gcdcllem1  16579  prmdvdsncoprmbd  16808  pceu  16928  4sqlem12  17038  vdwlem10  17072  vdwlem13  17075  vdwnn  17080  drsdirfi  18383  0gisid  18751  grprida  18759  smndex1mgm  19006  smndex1mndlem  19008  dfgrp2  19073  dfgrp3lem  19148  cyccom  19318  gaorb  19421  psgnunilem3  19610  psgnunilem4  19611  psgneu  19620  pj1eu  19810  efgsfo  19853  cyggeninv  19997  cygabl  20005  pgpfac1lem5  20195  pgpfac1  20196  pgpfaclem2  20198  isdrng4  20889  isdrng3lem2  20902  lss1d  21134  lspsneq  21296  lspsolvlem  21316  lbsextlem2  21333  cygznlem3  21769  mplcoe5lem  22240  pmatcollpw3fi1lem2  22994  ordtrest2lem  23410  cnprest  23496  1stcfb  23652  1stcelcls  23669  elpt  23780  fbssfi  24045  fgcl  24086  rnelfmlem  24160  fmfnfmlem3  24164  txflf  24214  alexsubb  24254  alexsubALTlem4  24258  isucn2  24486  icccmplem2  25032  ply1divex  26345  coeeu  26433  plydivex  26509  aannenlem2  26543  ulmcau  26609  ulmbdd  26612  dchrptlem2  27480  bposlem9  27507  2lgslem1b  27607  pntibndlem3  27807  pntlemi  27819  pntlemp  27825  pntleml  27826  pnt3  27827  nosupprefixmo  27915  noinfprefixmo  27916  nosupcbv  27917  nosupdm  27919  nosupfv  27921  nosupres  27922  nosupbnd1lem1  27923  nosupbnd1lem4  27926  noinfcbv  27932  noinfdm  27934  noinfbnd1lem4  27941  cofslts  28162  coinitslts  28163  addsval2  28207  addcuts  28222  addsunif  28246  norecdiv  28434  recsne0  28436  bdayn0sf1o  28614  dfnns2  28616  n0seo  28665  pw2recs  28682  bdayfinbndcbv  28710  bdayfinbndlem1  28711  bdayfinbndlem2  28712  recut  28738  readdscl  28743  legval  28904  legov  28905  legov2  28906  outpasch  29088  lnopp2hpgb  29096  colopp  29102  elplngid  29115  lnincplng  29117  plngcp  29119  plngrot  29123  nhpmirhp  29131  lnperpexs  29165  ragraghl  29200  tgaaddcpbllem2  29204  tgaaddcpbllem3  29205  prlnghpg  29251  prlngmo  29259  tgaltai  29272  erclwwlksym  30439  erclwwlktr  30440  erclwwlknsym  30488  erclwwlkntr  30489  eleclclwwlkn  30494  hashecclwwlkn1  30495  umgrhashecclwwlk  30496  grpoidinvlem3  30929  ubthlem3  31295  norm1exi  31673  pjhthmo  31725  cdjreui  32855  cdj3i  32864  infxrge0glb  33180  mndlrinvb  33409  gsumwrd2dccatlem  33461  cyc3genpm  33536  isarchi3  33571  archiabl  33582  erler  33649  rlocisunit  33660  1arithidomlem1  33889  1arithidom  33891  1arithufdlem2  33899  1arithufdlem3  33900  1arithufd  33902  fldext2chn  34182  constrconj  34199  constrextdg2lem  34202  constrextdg2  34203  constrfiss  34205  zarclsun  34324  ordtrest2NEWlem  34376  lmxrge0  34406  esumcvg  34540  esum2d  34547  eulerpartlems  34815  eulerpartlemgvv  34831  onvf1odlem2  35645  connpconn  35764  cvmlift2lem12  35843  cvmlift2lem13  35844  cvmlift3lem2  35849  cvmlift3lem7  35854  cvmlift3  35857  fmlasuc  35915  fmla1  35916  satffunlem1lem1  35931  satffunlem2lem1  35933  r1peuqusdeg1  36172  funtransport  36560  funray  36669  funline  36671  fnessref  36925  neibastop2  36929  dissneqlem  38043  dissneq  38044  pibt2  38120  ptrest  38327  poimirlem27  38355  poimirlem32  38360  ismblfin  38369  volsupnfl  38373  itg2addnclem  38379  unirep  38423  filbcmb  38449  sdclem1  38452  sdc  38453  fdc  38454  incsequz  38457  heibor1lem  38518  heiborlem10  38529  isgrpda  38664  isdrngo2  38667  prnc  38776  prtlem13  39700  prtlem15  39707  lshpsmreu  39941  lshpkrlem1  39942  lshpkrlem3  39944  pclfinN  40732  4atex  40908  dihglblem2N  42126  lcfl7N  42333  lcf1o  42383  supinf  43068  fimgmcyclem  43359  mzpcompact2lem  43540  eldioph3  43555  diophrex  43564  rexrabdioph  43579  eldioph4i  43597  aomclem8  43846  hbtlem2  43909  rngunsnply  43954  onsucrn  44056  iunrelexpuztr  44503  ntrclsneine0lem  44848  rexlimddvcbvw  44988  cpcoll2d  45027  mnuprdlem3  45042  dvconstbi  45102  expgrowth  45103  wessf1ornlem  45961  rnmptlb  46016  rnmptbdd  46018  rnmptbd2  46022  rnmptbd  46029  rexabsle  46191  uzub  46203  infrpgernmpt  46237  limcperiod  46402  limsupre  46413  limsupbnd1f  46458  climinf2  46479  climinfmpt  46487  limsupubuzmpt  46491  limsupmnf  46493  limsupre2  46497  limsupmnfuzlem  46498  limsupmnfuz  46499  limsupre2mpt  46502  limsupre3  46505  limsupre3mpt  46506  limsupre3uz  46508  limsupreuz  46509  limsupreuzmpt  46511  supcnvlimsup  46512  climuz  46516  lmbr3  46519  climrescn  46520  limsuplt2  46525  liminflelimsup  46548  limsupgt  46550  liminfreuz  46575  liminflt  46577  xlimpnfxnegmnf  46586  xlimmnf  46613  xlimpnf  46614  xlimmnfmpt  46615  xlimpnfmpt  46616  dfxlim2  46620  cncfshiftioo  46664  itgiccshift  46752  itgperiod  46753  fourierdlem42  46921  fourierdlem48  46926  fourierdlem81  46959  fourierdlem92  46970  fourierdlem96  46974  fourierdlem97  46975  fourierdlem98  46976  fourierdlem99  46977  fourierdlem105  46983  fourierdlem108  46986  fourierdlem110  46988  fourierdlem112  46990  fourierdlem113  46991  meaiunincf  47255  meaiuninc3v  47256  hoidmvval0  47359  ovnhoi  47375  ovolval5lem3  47426  ovolval5  47427  smfsup  47586  smfinflem  47589  smfinf  47590  fsetsnfo  47848  2reuimp0  47909  nndivides2  48179  imaelsetpreimafv  48202  imasetpreimafvbijlemfo  48212  fundcmpsurinj  48216  fundcmpsurbijinj  48217  fmtnofac2lem  48378  2zlidl  49062  2zrngamgm  49067  2zrngagrp  49071  2zrngmmgm  49074  eenglngeehlnmlem1  49574  upciclem4  50004