Theorem cbvrexvw 3241

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

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

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 2147

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

This theorem is used by:  cbvrex2vw  3245  reu7  3690  cbviunv  4997  disjiund  5094  reusv3  5370  xpdifid  6160  xpdifcnvepel  6161  fliftfun  7313  funcnvuni  7929  fiunlem  7939  poseq  8156  soseq  8157  nneob  8644  coflton  8659  cofon1  8660  cofon2  8661  pssnn  9163  frfi  9255  finsschain  9326  marypha1lem  9403  supmo  9422  suplub2  9431  infmo  9467  ordtypelem3  9492  ordtypelem9  9498  wemaplem1  9518  brwdom3  9554  unwdomg  9556  cantnf  9672  ttrcltr  9695  trcl  9707  infxpenc2  10025  aceq2  10122  dfac5lem4  10129  kmlem9  10161  kmlem14  10166  fin23lem26  10327  fin1a2lem13  10414  axdc3lem3  10454  winainflem  10702  axgroth4  10841  suprlub  12203  supaddc  12206  supadd  12207  supmul1  12208  supmullem1  12209  supmullem2  12210  supmul  12211  ublbneg  12982  zsupss  12986  xrsupsslem  13359  xrinfmsslem  13360  rexanre  15434  rexuzre  15440  rexico  15441  caurcvg2  15765  caucvgb  15767  summolem2  15802  summo  15803  mertens  15975  prodmolem2  16022  prodmo  16023  odd2np1lem  16430  gcdcllem1  16589  prmdvdsncoprmbd  16818  pceu  16938  4sqlem12  17048  vdwlem10  17082  vdwlem13  17085  vdwnn  17090  drsdirfi  18393  0gisid  18761  grprida  18769  smndex1mgm  19019  smndex1mndlem  19021  dfgrp2  19086  dfgrp3lem  19161  cyccom  19331  gaorb  19434  psgnunilem3  19623  psgnunilem4  19624  psgneu  19633  pj1eu  19823  efgsfo  19866  cyggeninv  20010  cygabl  20018  pgpfac1lem5  20208  pgpfac1  20209  pgpfaclem2  20211  isdrng4  20902  isdrng3lem2  20915  lss1d  21147  lspsneq  21309  lspsolvlem  21329  lbsextlem2  21346  cygznlem3  21782  mplcoe5lem  22255  pmatcollpw3fi1lem2  23012  ordtrest2lem  23428  cnprest  23514  1stcfb  23670  1stcelcls  23687  elpt  23798  fbssfi  24063  fgcl  24104  rnelfmlem  24178  fmfnfmlem3  24182  txflf  24232  alexsubb  24272  alexsubALTlem4  24276  isucn2  24504  icccmplem2  25050  ply1divex  26362  coeeu  26451  plydivex  26527  aannenlem2  26565  ulmcau  26631  ulmbdd  26634  dchrptlem2  27501  bposlem9  27528  2lgslem1b  27628  pntibndlem3  27828  pntlemi  27840  pntlemp  27846  pntleml  27847  pnt3  27848  nosupprefixmo  27936  noinfprefixmo  27937  nosupcbv  27938  nosupdm  27940  nosupfv  27942  nosupres  27943  nosupbnd1lem1  27944  nosupbnd1lem4  27947  noinfcbv  27953  noinfdm  27955  noinfbnd1lem4  27962  cofslts  28183  coinitslts  28184  addsval2  28228  addcuts  28243  addsunif  28267  norecdiv  28455  recsne0  28457  bdayn0sf1o  28635  dfnns2  28637  n0seo  28686  pw2recs  28703  bdayfinbndcbv  28731  bdayfinbndlem1  28732  bdayfinbndlem2  28733  recut  28759  readdscl  28764  legval  28926  legov  28927  legov2  28928  outpasch  29112  lnopp2hpgb  29120  colopp  29126  elplngid  29139  lnincplng  29141  plngcp  29143  plngrot  29147  nhpmirhp  29155  lnperpexs  29189  ragraghl  29225  tgaaddcpbllem2  29229  tgaaddcpbllem3  29230  tgaaddcpbl2  29232  angmgmaddeu1  29258  angmgmaddcl  29270  prlnghpg  29303  prlngmo  29311  tgaltai  29324  erclwwlksym  30491  erclwwlktr  30492  erclwwlknsym  30540  erclwwlkntr  30541  eleclclwwlkn  30546  hashecclwwlkn1  30547  umgrhashecclwwlk  30548  grpoidinvlem3  30987  ubthlem3  31353  norm1exi  31731  pjhthmo  31783  cdjreui  32913  cdj3i  32922  infxrge0glb  33236  mndlrinvb  33465  gsumwrd2dccatlem  33517  cyc3genpm  33592  isarchi3  33627  archiabl  33638  erler  33705  rlocisunit  33716  1arithidomlem1  33945  1arithidom  33947  1arithufdlem2  33955  1arithufdlem3  33956  1arithufd  33958  fldext2chn  34238  constrconj  34255  constrextdg2lem  34258  constrextdg2  34259  constrfiss  34261  zarclsun  34380  ordtrest2NEWlem  34432  lmxrge0  34462  esumcvg  34596  esum2d  34603  eulerpartlems  34871  eulerpartlemgvv  34887  onvf1odlem2  35701  connpconn  35814  cvmlift2lem12  35893  cvmlift2lem13  35894  cvmlift3lem2  35899  cvmlift3lem7  35904  cvmlift3  35907  fmlasuc  35965  fmla1  35966  satffunlem1lem1  35981  satffunlem2lem1  35983  r1peuqusdeg1  36222  funtransport  36611  funray  36720  funline  36722  fnessref  36976  neibastop2  36980  dissneqlem  38094  dissneq  38095  pibt2  38171  ptrest  38368  poimirlem27  38396  poimirlem32  38401  ismblfin  38410  volsupnfl  38414  itg2addnclem  38420  unirep  38464  filbcmb  38490  sdclem1  38493  sdc  38494  fdc  38495  incsequz  38498  heibor1lem  38559  heiborlem10  38570  isgrpda  38705  isdrngo2  38708  prnc  38817  prtlem13  39741  prtlem15  39748  lshpsmreu  39982  lshpkrlem1  39983  lshpkrlem3  39985  pclfinN  40773  4atex  40949  dihglblem2N  42167  lcfl7N  42374  lcf1o  42424  supinf  43109  fimgmcyclem  43415  mzpcompact2lem  43596  eldioph3  43611  diophrex  43620  rexrabdioph  43635  eldioph4i  43653  aomclem8  43902  hbtlem2  43965  rngunsnply  44010  onsucrn  44112  iunrelexpuztr  44559  ntrclsneine0lem  44904  rexlimddvcbvw  45044  cpcoll2d  45083  mnuprdlem3  45098  dvconstbi  45158  expgrowth  45159  wessf1ornlem  46017  rnmptlb  46072  rnmptbdd  46074  rnmptbd2  46078  rnmptbd  46085  rexabsle  46247  uzub  46259  infrpgernmpt  46293  limcperiod  46458  limsupre  46469  limsupbnd1f  46514  climinf2  46535  climinfmpt  46543  limsupubuzmpt  46547  limsupmnf  46549  limsupre2  46553  limsupmnfuzlem  46554  limsupmnfuz  46555  limsupre2mpt  46558  limsupre3  46561  limsupre3mpt  46562  limsupre3uz  46564  limsupreuz  46565  limsupreuzmpt  46567  supcnvlimsup  46568  climuz  46572  lmbr3  46575  climrescn  46576  limsuplt2  46581  liminflelimsup  46604  limsupgt  46606  liminfreuz  46631  liminflt  46633  xlimpnfxnegmnf  46642  xlimmnf  46669  xlimpnf  46670  xlimmnfmpt  46671  xlimpnfmpt  46672  dfxlim2  46676  cncfshiftioo  46720  itgiccshift  46808  itgperiod  46809  fourierdlem42  46977  fourierdlem48  46982  fourierdlem81  47015  fourierdlem92  47026  fourierdlem96  47030  fourierdlem97  47031  fourierdlem98  47032  fourierdlem99  47033  fourierdlem105  47039  fourierdlem108  47042  fourierdlem110  47044  fourierdlem112  47046  fourierdlem113  47047  meaiunincf  47311  meaiuninc3v  47312  hoidmvval0  47415  ovnhoi  47431  ovolval5lem3  47482  ovolval5  47483  smfsup  47642  smfinflem  47645  smfinf  47646  fsetsnfo  47941  2reuimp0  48002  nndivides2  48272  imaelsetpreimafv  48295  imasetpreimafvbijlemfo  48305  fundcmpsurinj  48309  fundcmpsurbijinj  48310  fmtnofac2lem  48471  2zlidl  49155  2zrngamgm  49160  2zrngagrp  49164  2zrngmmgm  49167  eenglngeehlnmlem1  49667  upciclem4  50095