Theorem cbvrexvw 3373

Description: Change the bound variable of a restricted existential quantifier using implicit substitution. Version of cbvrexv 3378 with a disjoint variable condition, which does not require ax-10 2139, ax-11 2156, ax-12 2173, ax-13 2372. (Contributed by NM, 2-Jun-1998.) (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 2821	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvralvw.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	1, 2	anbi12d 630	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑦 ∈ 𝐴 ∧ 𝜓)))
4	3	cbvexvw 2041	. 2 ⊢ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ 𝜓))
5		df-rex 3069	. 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
6		df-rex 3069	. 2 ⊢ (∃𝑦 ∈ 𝐴 𝜓 ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ 𝜓))
7	4, 5, 6	3bitr4i 302	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395  ∃wex 1783   ∈ wcel 2108  ∃wrex 3064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-clel 2817  df-rex 3069

This theorem is referenced by:  cbvrex2vw  3386  reu7  3662  disjiund  5060  reusv3  5323  xpdifid  6060  fliftfun  7163  funcnvuni  7752  fiunlem  7758  nneob  8446  pssnn  8913  pssnnOLD  8969  frfi  8989  finsschain  9056  marypha1lem  9122  supmo  9141  suplub2  9150  infmo  9184  ordtypelem3  9209  ordtypelem9  9215  wemaplem1  9235  brwdom3  9271  unwdomg  9273  cantnf  9381  trcl  9417  infxpenc2  9709  aceq2  9806  dfac5lem4  9813  kmlem9  9845  kmlem14  9850  fin23lem26  10012  fin1a2lem13  10099  axdc3lem3  10139  winainflem  10380  axgroth4  10519  suprlub  11869  supaddc  11872  supadd  11873  supmul1  11874  supmullem1  11875  supmullem2  11876  supmul  11877  ublbneg  12602  zsupss  12606  xrsupsslem  12970  xrinfmsslem  12971  rexanre  14986  rexuzre  14992  rexico  14993  caurcvg2  15317  caucvgb  15319  summolem2  15356  summo  15357  mertens  15526  prodmolem2  15573  prodmo  15574  odd2np1lem  15977  gcdcllem1  16134  prmdvdsncoprmbd  16359  pceu  16475  4sqlem12  16585  vdwlem10  16619  vdwlem13  16622  vdwnn  16627  drsdirfi  17938  grpridd  18274  smndex1mgm  18461  smndex1mndlem  18463  dfgrp2  18519  dfgrp3lem  18588  cyccom  18737  gaorb  18828  psgnunilem3  19019  psgnunilem4  19020  psgneu  19029  pj1eu  19217  efgsfo  19260  cyggeninv  19398  cygabl  19406  pgpfac1lem5  19597  pgpfac1  19598  pgpfaclem2  19600  lss1d  20140  lspsneq  20299  lspsolvlem  20319  lbsextlem2  20336  cygznlem3  20689  mplcoe5lem  21150  pmatcollpw3fi1lem2  21844  ordtrest2lem  22262  cnprest  22348  1stcfb  22504  1stcelcls  22520  elpt  22631  fbssfi  22896  fgcl  22937  rnelfmlem  23011  fmfnfmlem3  23015  txflf  23065  alexsubb  23105  alexsubALTlem4  23109  isucn2  23339  icccmplem2  23892  ply1divex  25206  coeeu  25291  plydivex  25362  aannenlem2  25394  ulmcau  25459  ulmbdd  25462  dchrptlem2  26318  bposlem9  26345  2lgslem1b  26445  pntibndlem3  26645  pntlemi  26657  pntlemp  26663  pntleml  26664  pnt3  26665  legval  26849  legov  26850  legov2  26851  outpasch  27020  lnopp2hpgb  27028  colopp  27034  erclwwlksym  28286  erclwwlktr  28287  erclwwlknsym  28335  erclwwlkntr  28336  eleclclwwlkn  28341  hashecclwwlkn1  28342  umgrhashecclwwlk  28343  grpoidinvlem3  28769  ubthlem3  29135  norm1exi  29513  pjhthmo  29565  cdjreui  30695  cdj3i  30704  infxrge0glb  30990  cyc3genpm  31321  isarchi3  31343  archiabl  31354  zarclsun  31722  ordtrest2NEWlem  31774  lmxrge0  31804  esumcvg  31954  esum2d  31961  eulerpartlems  32227  eulerpartlemgvv  32243  connpconn  33097  cvmlift2lem12  33176  cvmlift2lem13  33177  cvmlift3lem2  33182  cvmlift3lem7  33187  cvmlift3  33190  fmlasuc  33248  fmla1  33249  satffunlem1lem1  33264  satffunlem2lem1  33266  ttrcltr  33702  poseq  33729  soseq  33730  nosupprefixmo  33830  noinfprefixmo  33831  nosupcbv  33832  nosupdm  33834  nosupfv  33836  nosupres  33837  nosupbnd1lem1  33838  nosupbnd1lem4  33841  noinfcbv  33847  noinfdm  33849  noinfbnd1lem4  33856  cofsslt  34015  coinitsslt  34016  funtransport  34260  funray  34369  funline  34371  fnessref  34473  neibastop2  34477  dissneqlem  35438  dissneq  35439  pibt2  35515  ptrest  35703  poimirlem27  35731  poimirlem32  35736  ismblfin  35745  volsupnfl  35749  itg2addnclem  35755  unirep  35798  filbcmb  35825  sdclem1  35828  sdc  35829  fdc  35830  incsequz  35833  heibor1lem  35894  heiborlem10  35905  isgrpda  36040  isdrngo2  36043  prnc  36152  prtlem13  36809  prtlem15  36816  lshpsmreu  37050  lshpkrlem1  37051  lshpkrlem3  37053  pclfinN  37841  4atex  38017  dihglblem2N  39235  lcfl7N  39442  lcf1o  39492  mzpcompact2lem  40489  eldioph3  40504  diophrex  40513  rexrabdioph  40532  eldioph4i  40550  aomclem8  40802  hbtlem2  40865  rngunsnply  40914  iunrelexpuztr  41216  ntrclsneine0lem  41563  rexlimddvcbvw  41706  cpcoll2d  41766  mnuprdlem3  41781  dvconstbi  41841  expgrowth  41842  wessf1ornlem  42611  rnmptlb  42677  rnmptbdd  42679  rnmptbd2  42684  rnmptbd  42691  rexabsle  42849  uzub  42861  infrpgernmpt  42895  limcperiod  43059  limsupre  43072  limsupbnd1f  43117  climinf2  43138  climinfmpt  43146  limsupubuzmpt  43150  limsupmnf  43152  limsupre2  43156  limsupmnfuzlem  43157  limsupmnfuz  43158  limsupre2mpt  43161  limsupre3  43164  limsupre3mpt  43165  limsupre3uz  43167  limsupreuz  43168  limsupreuzmpt  43170  supcnvlimsup  43171  climuz  43175  lmbr3  43178  climrescn  43179  limsuplt2  43184  liminflelimsup  43207  limsupgt  43209  liminfreuz  43234  liminflt  43236  xlimpnfxnegmnf  43245  xlimmnf  43272  xlimpnf  43273  xlimmnfmpt  43274  xlimpnfmpt  43275  dfxlim2  43279  cncfshiftioo  43323  itgiccshift  43411  itgperiod  43412  fourierdlem42  43580  fourierdlem48  43585  fourierdlem81  43618  fourierdlem92  43629  fourierdlem96  43633  fourierdlem97  43634  fourierdlem98  43635  fourierdlem99  43636  fourierdlem105  43642  fourierdlem108  43645  fourierdlem110  43647  fourierdlem112  43649  fourierdlem113  43650  meaiunincf  43911  meaiuninc3v  43912  hoidmvval0  44015  ovnhoi  44031  ovolval5lem3  44082  ovolval5  44083  smfsup  44234  smfinflem  44237  smfinf  44238  fsetsnfo  44434  2reuimp0  44493  imaelsetpreimafv  44735  imasetpreimafvbijlemfo  44745  fundcmpsurinj  44749  fundcmpsurbijinj  44750  fmtnofac2lem  44908  2zlidl  45380  2zrngamgm  45385  2zrngagrp  45389  2zrngmmgm  45392  eenglngeehlnmlem1  45971