Theorem cbvrexvw 3212

Description: Change the bound variable of a restricted existential quantifier using implicit substitution. Version of cbvrexv 3332 with a disjoint variable condition, which does not require ax-10 2146, ax-11 2162, ax-12 2182, ax-13 2374. (Contributed by NM, 2-Jun-1998.) Avoid ax-13 2374. (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 2816	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvralvw.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	1, 2	anbi12d 632	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑦 ∈ 𝐴 ∧ 𝜓)))
4	3	cbvexvw 2038	. 2 ⊢ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ 𝜓))
5		df-rex 3058	. 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
6		df-rex 3058	. 2 ⊢ (∃𝑦 ∈ 𝐴 𝜓 ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ 𝜓))
7	4, 5, 6	3bitr4i 303	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∃wex 1780   ∈ wcel 2113  ∃wrex 3057

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-clel 2808  df-rex 3058

This theorem is referenced by:  cbvrex2vw  3216  reu7  3687  cbviunv  4991  disjiund  5086  reusv3  5347  xpdifid  6123  fliftfun  7255  funcnvuni  7871  fiunlem  7883  poseq  8097  soseq  8098  nneob  8580  coflton  8595  cofon1  8596  cofon2  8597  pssnn  9089  frfi  9180  finsschain  9254  marypha1lem  9328  supmo  9347  suplub2  9356  infmo  9392  ordtypelem3  9417  ordtypelem9  9423  wemaplem1  9443  brwdom3  9479  unwdomg  9481  cantnf  9594  ttrcltr  9617  trcl  9629  infxpenc2  9924  aceq2  10021  dfac5lem4  10028  dfac5lem4OLD  10030  kmlem9  10061  kmlem14  10066  fin23lem26  10227  fin1a2lem13  10314  axdc3lem3  10354  winainflem  10595  axgroth4  10734  suprlub  12097  supaddc  12100  supadd  12101  supmul1  12102  supmullem1  12103  supmullem2  12104  supmul  12105  ublbneg  12837  zsupss  12841  xrsupsslem  13213  xrinfmsslem  13214  rexanre  15261  rexuzre  15267  rexico  15268  caurcvg2  15592  caucvgb  15594  summolem2  15630  summo  15631  mertens  15800  prodmolem2  15849  prodmo  15850  odd2np1lem  16258  gcdcllem1  16417  prmdvdsncoprmbd  16645  pceu  16765  4sqlem12  16875  vdwlem10  16909  vdwlem13  16912  vdwnn  16917  drsdirfi  18219  grprida  18591  smndex1mgm  18823  smndex1mndlem  18825  dfgrp2  18883  dfgrp3lem  18959  cyccom  19123  gaorb  19227  psgnunilem3  19416  psgnunilem4  19417  psgneu  19426  pj1eu  19616  efgsfo  19659  cyggeninv  19803  cygabl  19811  pgpfac1lem5  20001  pgpfac1  20002  pgpfaclem2  20004  lss1d  20905  lspsneq  21068  lspsolvlem  21088  lbsextlem2  21105  cygznlem3  21515  mplcoe5lem  21985  pmatcollpw3fi1lem2  22722  ordtrest2lem  23138  cnprest  23224  1stcfb  23380  1stcelcls  23396  elpt  23507  fbssfi  23772  fgcl  23813  rnelfmlem  23887  fmfnfmlem3  23891  txflf  23941  alexsubb  23981  alexsubALTlem4  23985  isucn2  24213  icccmplem2  24759  ply1divex  26089  coeeu  26177  plydivex  26252  aannenlem2  26284  ulmcau  26351  ulmbdd  26354  dchrptlem2  27223  bposlem9  27250  2lgslem1b  27350  pntibndlem3  27550  pntlemi  27562  pntlemp  27568  pntleml  27569  pnt3  27570  nosupprefixmo  27659  noinfprefixmo  27660  nosupcbv  27661  nosupdm  27663  nosupfv  27665  nosupres  27666  nosupbnd1lem1  27667  nosupbnd1lem4  27670  noinfcbv  27676  noinfdm  27678  noinfbnd1lem4  27685  cofsslt  27882  coinitsslt  27883  addsval2  27926  addscut  27941  addsunif  27965  norecdiv  28149  recsne0  28151  bdayn0sf1o  28315  dfnns2  28317  n0seo  28364  pw2recs  28381  recut  28418  readdscl  28421  legval  28582  legov  28583  legov2  28584  outpasch  28753  lnopp2hpgb  28761  colopp  28767  erclwwlksym  30022  erclwwlktr  30023  erclwwlknsym  30071  erclwwlkntr  30072  eleclclwwlkn  30077  hashecclwwlkn1  30078  umgrhashecclwwlk  30079  grpoidinvlem3  30507  ubthlem3  30873  norm1exi  31251  pjhthmo  31303  cdjreui  32433  cdj3i  32442  infxrge0glb  32773  mndlrinvb  33035  gsumwrd2dccatlem  33087  cyc3genpm  33162  isarchi3  33197  archiabl  33208  erler  33275  isdrng4  33305  1arithidomlem1  33544  1arithidom  33546  1arithufdlem2  33554  1arithufdlem3  33555  1arithufd  33557  fldext2chn  33813  constrconj  33830  constrextdg2lem  33833  constrextdg2  33834  constrfiss  33836  zarclsun  33955  ordtrest2NEWlem  34007  lmxrge0  34037  esumcvg  34171  esum2d  34178  eulerpartlems  34445  eulerpartlemgvv  34461  onvf1odlem2  35220  connpconn  35351  cvmlift2lem12  35430  cvmlift2lem13  35431  cvmlift3lem2  35436  cvmlift3lem7  35441  cvmlift3  35444  fmlasuc  35502  fmla1  35503  satffunlem1lem1  35518  satffunlem2lem1  35520  r1peuqusdeg1  35759  funtransport  36147  funray  36256  funline  36258  fnessref  36473  neibastop2  36477  dissneqlem  37457  dissneq  37458  pibt2  37534  ptrest  37732  poimirlem27  37760  poimirlem32  37765  ismblfin  37774  volsupnfl  37778  itg2addnclem  37784  unirep  37827  filbcmb  37853  sdclem1  37856  sdc  37857  fdc  37858  incsequz  37861  heibor1lem  37922  heiborlem10  37933  isgrpda  38068  isdrngo2  38071  prnc  38180  prtlem13  39040  prtlem15  39047  lshpsmreu  39281  lshpkrlem1  39282  lshpkrlem3  39284  pclfinN  40072  4atex  40248  dihglblem2N  41466  lcfl7N  41673  lcf1o  41723  supinf  42412  fimgmcyclem  42703  mzpcompact2lem  42908  eldioph3  42923  diophrex  42932  rexrabdioph  42951  eldioph4i  42969  aomclem8  43218  hbtlem2  43281  rngunsnply  43326  onsucrn  43428  iunrelexpuztr  43876  ntrclsneine0lem  44221  rexlimddvcbvw  44363  cpcoll2d  44416  mnuprdlem3  44431  dvconstbi  44491  expgrowth  44492  wessf1ornlem  45345  rnmptlb  45403  rnmptbdd  45405  rnmptbd2  45409  rnmptbd  45416  rexabsle  45579  uzub  45591  infrpgernmpt  45625  limcperiod  45790  limsupre  45801  limsupbnd1f  45846  climinf2  45867  climinfmpt  45875  limsupubuzmpt  45879  limsupmnf  45881  limsupre2  45885  limsupmnfuzlem  45886  limsupmnfuz  45887  limsupre2mpt  45890  limsupre3  45893  limsupre3mpt  45894  limsupre3uz  45896  limsupreuz  45897  limsupreuzmpt  45899  supcnvlimsup  45900  climuz  45904  lmbr3  45907  climrescn  45908  limsuplt2  45913  liminflelimsup  45936  limsupgt  45938  liminfreuz  45963  liminflt  45965  xlimpnfxnegmnf  45974  xlimmnf  46001  xlimpnf  46002  xlimmnfmpt  46003  xlimpnfmpt  46004  dfxlim2  46008  cncfshiftioo  46052  itgiccshift  46140  itgperiod  46141  fourierdlem42  46309  fourierdlem48  46314  fourierdlem81  46347  fourierdlem92  46358  fourierdlem96  46362  fourierdlem97  46363  fourierdlem98  46364  fourierdlem99  46365  fourierdlem105  46371  fourierdlem108  46374  fourierdlem110  46376  fourierdlem112  46378  fourierdlem113  46379  meaiunincf  46643  meaiuninc3v  46644  hoidmvval0  46747  ovnhoi  46763  ovolval5lem3  46814  ovolval5  46815  smfsup  46974  smfinflem  46977  smfinf  46978  nthrucw  47046  fsetsnfo  47215  2reuimp0  47276  imaelsetpreimafv  47557  imasetpreimafvbijlemfo  47567  fundcmpsurinj  47571  fundcmpsurbijinj  47572  fmtnofac2lem  47730  2zlidl  48402  2zrngamgm  48407  2zrngagrp  48411  2zrngmmgm  48414  eenglngeehlnmlem1  48899  upciclem4  49330