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 2177, ax-11 2193, ax-12 2212, 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 2069	. 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 1811   ∈ wcel 2144  ∃wrex 3086

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146

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

This theorem is used by:  cbvrex2vw  3245  reu7  3689  cbviunv  4996  disjiund  5093  reusv3  5367  xpdifid  6161  xpdifcnvepel  6162  fliftfun  7324  funcnvuni  7948  fiunlem  7958  poseq  8181  soseq  8182  nneob  8672  coflton  8687  cofon1  8688  cofon2  8689  pssnn  9191  frfi  9283  finsschain  9355  marypha1lem  9432  supmo  9451  suplub2  9460  infmo  9496  ordtypelem3  9521  ordtypelem9  9527  wemaplem1  9547  brwdom3  9583  unwdomg  9585  cantnf  9701  ttrcltr  9724  trcl  9736  infxpenc2  10108  aceq2  10205  dfac5lem4  10212  kmlem9  10244  kmlem14  10249  fin23lem26  10410  fin1a2lem13  10497  axdc3lem3  10537  winainflem  10785  axgroth4  10924  suprlub  12288  supaddc  12291  supadd  12292  supmul1  12293  supmullem1  12294  supmullem2  12295  supmul  12296  ublbneg  13067  zsupss  13071  xrsupsslem  13444  xrinfmsslem  13445  rexanre  15523  rexuzre  15529  rexico  15530  caurcvg2  15854  caucvgb  15856  summolem2  15891  summo  15892  mertens  16064  prodmolem2  16111  prodmo  16112  odd2np1lem  16519  gcdcllem1  16678  prmdvdsncoprmbd  16912  pceu  17033  4sqlem12  17143  vdwlem10  17177  vdwlem13  17180  vdwnn  17185  drsdirfi  18488  0gisid  18857  grprida  18865  smndex1mgm  19115  smndex1mndlem  19117  dfgrp2  19182  dfgrp3lem  19257  cyccom  19427  gaorb  19530  psgnunilem3  19719  psgnunilem4  19720  psgneu  19729  pj1eu  19919  efgsfo  19962  cyggeninv  20106  cygabl  20114  pgpfac1lem5  20304  pgpfac1  20305  pgpfaclem2  20307  isdrng4  21001  isdrng3lem2  21015  lss1d  21247  lspsneq  21409  lspsolvlem  21429  lbsextlem2  21446  cygznlem3  21884  mplcoe5lem  22357  pmatcollpw3fi1lem2  23114  ordtrest2lem  23530  cnprest  23616  1stcfb  23772  1stcelcls  23789  elpt  23900  fbssfi  24165  fgcl  24206  rnelfmlem  24280  fmfnfmlem3  24284  txflf  24334  alexsubb  24374  alexsubALTlem4  24378  isucn2  24606  icccmplem2  25152  ply1divex  26464  coeeu  26553  plydivex  26627  aannenlem2  26665  ulmcau  26731  ulmbdd  26734  dchrptlem2  27601  bposlem9  27628  2lgslem1b  27728  pntibndlem3  27928  pntlemi  27940  pntlemp  27946  pntleml  27947  pnt3  27948  nosupprefixmo  28066  noinfprefixmo  28067  nosupcbv  28068  nosupdm  28070  nosupfv  28072  nosupres  28073  nosupbnd1lem1  28074  nosupbnd1lem4  28077  noinfcbv  28083  noinfdm  28085  noinfbnd1lem4  28092  cofslts  28313  coinitslts  28314  addsval2  28358  addcuts  28373  addsunif  28397  norecdiv  28585  recsne0  28587  bdayn0sf1o  28765  dfnns2  28767  n0seo  28816  pw2recs  28833  bdayfinbndcbv  28861  bdayfinbndlem1  28862  bdayfinbndlem2  28863  recut  28889  readdscl  28894  legval  29056  legov  29057  legov2  29058  outpasch  29242  lnopp2hpgb  29250  colopp  29256  elplngid  29269  lnincplng  29271  plngcp  29273  plngrot  29277  nhpmirhp  29285  lnperpexs  29319  ragraghl  29355  tgaaddcpbllem2  29359  tgaaddcpbllem3  29360  tgaaddcpbl2  29362  angmgmaddeu1  29388  angmgmaddcl  29400  prlnghpg  29433  prlngmo  29441  tgaltai  29454  erclwwlksym  30621  erclwwlktr  30622  erclwwlknsym  30670  erclwwlkntr  30671  eleclclwwlkn  30676  hashecclwwlkn1  30677  umgrhashecclwwlk  30678  grpoidinvlem3  31117  ubthlem3  31483  norm1exi  31861  pjhthmo  31913  cdjreui  33043  cdj3i  33052  infxrge0glb  33407  mndlrinvb  33636  gsumwrd2dccatlem  33688  cyc3genpm  33763  isarchi3  33798  archiabl  33809  erler  33876  rlocisunit  33887  1arithidomlem1  34117  1arithidom  34119  1arithufdlem2  34127  1arithufdlem3  34128  1arithufd  34130  fldext2chn  34410  constrconj  34427  constrextdg2lem  34430  constrextdg2  34431  constrfiss  34433  zarclsun  34552  ordtrest2NEWlem  34604  lmxrge0  34634  esumcvg  34768  esum2d  34775  eulerpartlems  35042  eulerpartlemgvv  35058  onvf1odlem2  35955  connpconn  36090  cvmlift2lem12  36169  cvmlift2lem13  36170  cvmlift3lem2  36175  cvmlift3lem7  36180  cvmlift3  36183  fmlasuc  36241  fmla1  36242  satffunlem1lem1  36257  satffunlem2lem1  36259  r1peuqusdeg1  36498  funtransport  36892  funray  37001  funline  37003  fnessref  37241  neibastop2  37245  dissneqlem  38372  dissneq  38373  pibt2  38449  ptrest  38646  poimirlem27  38674  poimirlem32  38679  ismblfin  38688  volsupnfl  38692  itg2addnclem  38698  unirep  38757  filbcmb  38783  sdclem1  38786  sdc  38787  fdc  38788  incsequz  38791  heibor1lem  38852  heiborlem10  38863  isgrpda  38998  isdrngo2  39001  prnc  39110  prtlem13  40034  prtlem15  40041  lshpsmreu  40275  lshpkrlem1  40276  lshpkrlem3  40278  pclfinN  41066  4atex  41242  dihglblem2N  42460  lcfl7N  42667  lcf1o  42717  supinf  43402  fimgmcyclem  43706  mzpcompact2lem  43871  eldioph3  43886  diophrex  43895  rexrabdioph  43910  eldioph4i  43928  aomclem8  44172  hbtlem2  44235  rngunsnply  44280  onsucrn  44382  iunrelexpuztr  44828  ntrclsneine0lem  45173  rexlimddvcbvw  45313  cpcoll2d  45352  mnuprdlem3  45367  dvconstbi  45427  expgrowth  45428  wessf1ornlem  46308  rnmptlb  46363  rnmptbdd  46365  rnmptbd2  46369  rnmptbd  46376  rexabsle  46537  uzub  46549  infrpgernmpt  46583  limcperiod  46748  limsupre  46759  limsupbnd1f  46804  climinf2  46825  climinfmpt  46833  limsupubuzmpt  46837  limsupmnf  46839  limsupre2  46843  limsupmnfuzlem  46844  limsupmnfuz  46845  limsupre2mpt  46848  limsupre3  46851  limsupre3mpt  46852  limsupre3uz  46854  limsupreuz  46855  limsupreuzmpt  46857  supcnvlimsup  46858  climuz  46862  lmbr3  46865  climrescn  46866  limsuplt2  46871  liminflelimsup  46894  limsupgt  46896  liminfreuz  46921  liminflt  46923  xlimpnfxnegmnf  46932  xlimmnf  46959  xlimpnf  46960  xlimmnfmpt  46961  xlimpnfmpt  46962  dfxlim2  46966  cncfshiftioo  47010  itgiccshift  47098  itgperiod  47099  fourierdlem42  47267  fourierdlem48  47272  fourierdlem81  47305  fourierdlem92  47316  fourierdlem96  47320  fourierdlem97  47321  fourierdlem98  47322  fourierdlem99  47323  fourierdlem105  47329  fourierdlem108  47332  fourierdlem110  47334  fourierdlem112  47336  fourierdlem113  47337  meaiunincf  47601  meaiuninc3v  47602  hoidmvval0  47705  ovnhoi  47721  ovolval5lem3  47772  ovolval5  47773  smfsup  47932  smfinflem  47935  smfinf  47936  fsetsnfo  48231  2reuimp0  48293  nndivides2  48562  imaelsetpreimafv  48585  imasetpreimafvbijlemfo  48595  fundcmpsurinj  48599  fundcmpsurbijinj  48600  fmtnofac2lem  48761  2zlidl  49445  2zrngamgm  49450  2zrngagrp  49454  2zrngmmgm  49457  eenglngeehlnmlem1  49958  upciclem4  50393