Theorem cbvrexvw 3244

Description: Change the bound variable of a restricted existential quantifier using implicit substitution. Version of cbvrexv 3373 with a disjoint variable condition, which does not require ax-10 2141, ax-11 2158, ax-12 2178, ax-13 2380. (Contributed by NM, 2-Jun-1998.) Avoid ax-13 2380. (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 2827	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvralvw.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	1, 2	anbi12d 631	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑦 ∈ 𝐴 ∧ 𝜓)))
4	3	cbvexvw 2036	. 2 ⊢ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ 𝜓))
5		df-rex 3077	. 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
6		df-rex 3077	. 2 ⊢ (∃𝑦 ∈ 𝐴 𝜓 ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ 𝜓))
7	4, 5, 6	3bitr4i 303	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∃wex 1777   ∈ wcel 2108  ∃wrex 3076

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-clel 2819  df-rex 3077

This theorem is referenced by:  cbvrex2vw  3248  reu7  3754  cbviunv  5063  disjiund  5157  reusv3  5423  xpdifid  6199  fliftfun  7348  funcnvuni  7972  fiunlem  7982  poseq  8199  soseq  8200  nneob  8712  coflton  8727  cofon1  8728  cofon2  8729  pssnn  9234  frfi  9349  finsschain  9429  marypha1lem  9502  supmo  9521  suplub2  9530  infmo  9564  ordtypelem3  9589  ordtypelem9  9595  wemaplem1  9615  brwdom3  9651  unwdomg  9653  cantnf  9762  ttrcltr  9785  trcl  9797  infxpenc2  10091  aceq2  10188  dfac5lem4  10195  dfac5lem4OLD  10197  kmlem9  10228  kmlem14  10233  fin23lem26  10394  fin1a2lem13  10481  axdc3lem3  10521  winainflem  10762  axgroth4  10901  suprlub  12259  supaddc  12262  supadd  12263  supmul1  12264  supmullem1  12265  supmullem2  12266  supmul  12267  ublbneg  12998  zsupss  13002  xrsupsslem  13369  xrinfmsslem  13370  rexanre  15395  rexuzre  15401  rexico  15402  caurcvg2  15726  caucvgb  15728  summolem2  15764  summo  15765  mertens  15934  prodmolem2  15983  prodmo  15984  odd2np1lem  16388  gcdcllem1  16545  prmdvdsncoprmbd  16774  pceu  16893  4sqlem12  17003  vdwlem10  17037  vdwlem13  17040  vdwnn  17045  drsdirfi  18375  grprida  18713  smndex1mgm  18942  smndex1mndlem  18944  dfgrp2  19002  dfgrp3lem  19078  cyccom  19243  gaorb  19347  psgnunilem3  19538  psgnunilem4  19539  psgneu  19548  pj1eu  19738  efgsfo  19781  cyggeninv  19925  cygabl  19933  pgpfac1lem5  20123  pgpfac1  20124  pgpfaclem2  20126  lss1d  20984  lspsneq  21147  lspsolvlem  21167  lbsextlem2  21184  cygznlem3  21611  mplcoe5lem  22080  pmatcollpw3fi1lem2  22814  ordtrest2lem  23232  cnprest  23318  1stcfb  23474  1stcelcls  23490  elpt  23601  fbssfi  23866  fgcl  23907  rnelfmlem  23981  fmfnfmlem3  23985  txflf  24035  alexsubb  24075  alexsubALTlem4  24079  isucn2  24309  icccmplem2  24864  ply1divex  26196  coeeu  26284  plydivex  26357  aannenlem2  26389  ulmcau  26456  ulmbdd  26459  dchrptlem2  27327  bposlem9  27354  2lgslem1b  27454  pntibndlem3  27654  pntlemi  27666  pntlemp  27672  pntleml  27673  pnt3  27674  nosupprefixmo  27763  noinfprefixmo  27764  nosupcbv  27765  nosupdm  27767  nosupfv  27769  nosupres  27770  nosupbnd1lem1  27771  nosupbnd1lem4  27774  noinfcbv  27780  noinfdm  27782  noinfbnd1lem4  27789  cofsslt  27970  coinitsslt  27971  addsval2  28014  addscut  28029  addsunif  28053  norecdiv  28234  dfnns2  28380  n0seo  28423  recut  28446  readdscl  28449  legval  28610  legov  28611  legov2  28612  outpasch  28781  lnopp2hpgb  28789  colopp  28795  erclwwlksym  30053  erclwwlktr  30054  erclwwlknsym  30102  erclwwlkntr  30103  eleclclwwlkn  30108  hashecclwwlkn1  30109  umgrhashecclwwlk  30110  grpoidinvlem3  30538  ubthlem3  30904  norm1exi  31282  pjhthmo  31334  cdjreui  32464  cdj3i  32473  infxrge0glb  32772  mndlrinvb  33011  cyc3genpm  33145  isarchi3  33167  archiabl  33178  erler  33237  isdrng4  33264  1arithidomlem1  33528  1arithidom  33530  1arithufdlem2  33538  1arithufdlem3  33539  1arithufd  33541  fldext2chn  33719  constrconj  33735  zarclsun  33816  ordtrest2NEWlem  33868  lmxrge0  33898  esumcvg  34050  esum2d  34057  eulerpartlems  34325  eulerpartlemgvv  34341  connpconn  35203  cvmlift2lem12  35282  cvmlift2lem13  35283  cvmlift3lem2  35288  cvmlift3lem7  35293  cvmlift3  35296  fmlasuc  35354  fmla1  35355  satffunlem1lem1  35370  satffunlem2lem1  35372  r1peuqusdeg1  35611  funtransport  35995  funray  36104  funline  36106  fnessref  36323  neibastop2  36327  dissneqlem  37306  dissneq  37307  pibt2  37383  ptrest  37579  poimirlem27  37607  poimirlem32  37612  ismblfin  37621  volsupnfl  37625  itg2addnclem  37631  unirep  37674  filbcmb  37700  sdclem1  37703  sdc  37704  fdc  37705  incsequz  37708  heibor1lem  37769  heiborlem10  37780  isgrpda  37915  isdrngo2  37918  prnc  38027  prtlem13  38824  prtlem15  38831  lshpsmreu  39065  lshpkrlem1  39066  lshpkrlem3  39068  pclfinN  39857  4atex  40033  dihglblem2N  41251  lcfl7N  41458  lcf1o  41508  supinf  42237  fimgmcyclem  42488  mzpcompact2lem  42707  eldioph3  42722  diophrex  42731  rexrabdioph  42750  eldioph4i  42768  aomclem8  43018  hbtlem2  43081  rngunsnply  43130  onsucrn  43233  iunrelexpuztr  43681  ntrclsneine0lem  44026  rexlimddvcbvw  44168  cpcoll2d  44228  mnuprdlem3  44243  dvconstbi  44303  expgrowth  44304  wessf1ornlem  45092  rnmptlb  45152  rnmptbdd  45154  rnmptbd2  45158  rnmptbd  45165  rexabsle  45334  uzub  45346  infrpgernmpt  45380  limcperiod  45549  limsupre  45562  limsupbnd1f  45607  climinf2  45628  climinfmpt  45636  limsupubuzmpt  45640  limsupmnf  45642  limsupre2  45646  limsupmnfuzlem  45647  limsupmnfuz  45648  limsupre2mpt  45651  limsupre3  45654  limsupre3mpt  45655  limsupre3uz  45657  limsupreuz  45658  limsupreuzmpt  45660  supcnvlimsup  45661  climuz  45665  lmbr3  45668  climrescn  45669  limsuplt2  45674  liminflelimsup  45697  limsupgt  45699  liminfreuz  45724  liminflt  45726  xlimpnfxnegmnf  45735  xlimmnf  45762  xlimpnf  45763  xlimmnfmpt  45764  xlimpnfmpt  45765  dfxlim2  45769  cncfshiftioo  45813  itgiccshift  45901  itgperiod  45902  fourierdlem42  46070  fourierdlem48  46075  fourierdlem81  46108  fourierdlem92  46119  fourierdlem96  46123  fourierdlem97  46124  fourierdlem98  46125  fourierdlem99  46126  fourierdlem105  46132  fourierdlem108  46135  fourierdlem110  46137  fourierdlem112  46139  fourierdlem113  46140  meaiunincf  46404  meaiuninc3v  46405  hoidmvval0  46508  ovnhoi  46524  ovolval5lem3  46575  ovolval5  46576  smfsup  46735  smfinflem  46738  smfinf  46739  fsetsnfo  46968  2reuimp0  47029  imaelsetpreimafv  47269  imasetpreimafvbijlemfo  47279  fundcmpsurinj  47283  fundcmpsurbijinj  47284  fmtnofac2lem  47442  2zlidl  47963  2zrngamgm  47968  2zrngagrp  47972  2zrngmmgm  47975  eenglngeehlnmlem1  48471