Theorem cbvrexvw 3231

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395  ∃wex 1774   ∈ wcel 2099  ∃wrex 3066

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1775  df-clel 2806  df-rex 3067

This theorem is referenced by:  cbvrex2vw  3235  reu7  3726  disjiund  5132  reusv3  5399  xpdifid  6166  fliftfun  7314  funcnvuni  7933  fiunlem  7939  poseq  8157  soseq  8158  nneob  8670  coflton  8685  cofon1  8686  cofon2  8687  pssnn  9186  pssnnOLD  9283  frfi  9306  finsschain  9377  marypha1lem  9450  supmo  9469  suplub2  9478  infmo  9512  ordtypelem3  9537  ordtypelem9  9543  wemaplem1  9563  brwdom3  9599  unwdomg  9601  cantnf  9710  ttrcltr  9733  trcl  9745  infxpenc2  10039  aceq2  10136  dfac5lem4  10143  kmlem9  10175  kmlem14  10180  fin23lem26  10342  fin1a2lem13  10429  axdc3lem3  10469  winainflem  10710  axgroth4  10849  suprlub  12202  supaddc  12205  supadd  12206  supmul1  12207  supmullem1  12208  supmullem2  12209  supmul  12210  ublbneg  12941  zsupss  12945  xrsupsslem  13312  xrinfmsslem  13313  rexanre  15319  rexuzre  15325  rexico  15326  caurcvg2  15650  caucvgb  15652  summolem2  15688  summo  15689  mertens  15858  prodmolem2  15905  prodmo  15906  odd2np1lem  16310  gcdcllem1  16467  prmdvdsncoprmbd  16692  pceu  16808  4sqlem12  16918  vdwlem10  16952  vdwlem13  16955  vdwnn  16960  drsdirfi  18290  grprida  18628  smndex1mgm  18852  smndex1mndlem  18854  dfgrp2  18912  dfgrp3lem  18987  cyccom  19151  gaorb  19251  psgnunilem3  19444  psgnunilem4  19445  psgneu  19454  pj1eu  19644  efgsfo  19687  cyggeninv  19831  cygabl  19839  pgpfac1lem5  20029  pgpfac1  20030  pgpfaclem2  20032  lss1d  20840  lspsneq  21003  lspsolvlem  21023  lbsextlem2  21040  cygznlem3  21496  mplcoe5lem  21970  pmatcollpw3fi1lem2  22682  ordtrest2lem  23100  cnprest  23186  1stcfb  23342  1stcelcls  23358  elpt  23469  fbssfi  23734  fgcl  23775  rnelfmlem  23849  fmfnfmlem3  23853  txflf  23903  alexsubb  23943  alexsubALTlem4  23947  isucn2  24177  icccmplem2  24732  ply1divex  26065  coeeu  26152  plydivex  26225  aannenlem2  26257  ulmcau  26324  ulmbdd  26327  dchrptlem2  27191  bposlem9  27218  2lgslem1b  27318  pntibndlem3  27518  pntlemi  27530  pntlemp  27536  pntleml  27537  pnt3  27538  nosupprefixmo  27626  noinfprefixmo  27627  nosupcbv  27628  nosupdm  27630  nosupfv  27632  nosupres  27633  nosupbnd1lem1  27634  nosupbnd1lem4  27637  noinfcbv  27643  noinfdm  27645  noinfbnd1lem4  27652  cofsslt  27831  coinitsslt  27832  addsval2  27873  addscut  27888  addsunif  27912  norecdiv  28083  recut  28217  readdscl  28220  legval  28381  legov  28382  legov2  28383  outpasch  28552  lnopp2hpgb  28560  colopp  28566  erclwwlksym  29824  erclwwlktr  29825  erclwwlknsym  29873  erclwwlkntr  29874  eleclclwwlkn  29879  hashecclwwlkn1  29880  umgrhashecclwwlk  29881  grpoidinvlem3  30309  ubthlem3  30675  norm1exi  31053  pjhthmo  31105  cdjreui  32235  cdj3i  32244  infxrge0glb  32529  cyc3genpm  32867  isarchi3  32889  archiabl  32900  isdrng4  32956  erler  32973  zarclsun  33465  ordtrest2NEWlem  33517  lmxrge0  33547  esumcvg  33699  esum2d  33706  eulerpartlems  33974  eulerpartlemgvv  33990  connpconn  34839  cvmlift2lem12  34918  cvmlift2lem13  34919  cvmlift3lem2  34924  cvmlift3lem7  34929  cvmlift3  34932  fmlasuc  34990  fmla1  34991  satffunlem1lem1  35006  satffunlem2lem1  35008  funtransport  35621  funray  35730  funline  35732  fnessref  35835  neibastop2  35839  dissneqlem  36813  dissneq  36814  pibt2  36890  ptrest  37086  poimirlem27  37114  poimirlem32  37119  ismblfin  37128  volsupnfl  37132  itg2addnclem  37138  unirep  37181  filbcmb  37207  sdclem1  37210  sdc  37211  fdc  37212  incsequz  37215  heibor1lem  37276  heiborlem10  37287  isgrpda  37422  isdrngo2  37425  prnc  37534  prtlem13  38334  prtlem15  38341  lshpsmreu  38575  lshpkrlem1  38576  lshpkrlem3  38578  pclfinN  39367  4atex  39543  dihglblem2N  40761  lcfl7N  40968  lcf1o  41018  mzpcompact2lem  42165  eldioph3  42180  diophrex  42189  rexrabdioph  42208  eldioph4i  42226  aomclem8  42479  hbtlem2  42542  rngunsnply  42591  onsucrn  42694  iunrelexpuztr  43143  ntrclsneine0lem  43488  rexlimddvcbvw  43630  cpcoll2d  43690  mnuprdlem3  43705  dvconstbi  43765  expgrowth  43766  wessf1ornlem  44552  rnmptlb  44613  rnmptbdd  44615  rnmptbd2  44619  rnmptbd  44626  rexabsle  44795  uzub  44807  infrpgernmpt  44841  limcperiod  45010  limsupre  45023  limsupbnd1f  45068  climinf2  45089  climinfmpt  45097  limsupubuzmpt  45101  limsupmnf  45103  limsupre2  45107  limsupmnfuzlem  45108  limsupmnfuz  45109  limsupre2mpt  45112  limsupre3  45115  limsupre3mpt  45116  limsupre3uz  45118  limsupreuz  45119  limsupreuzmpt  45121  supcnvlimsup  45122  climuz  45126  lmbr3  45129  climrescn  45130  limsuplt2  45135  liminflelimsup  45158  limsupgt  45160  liminfreuz  45185  liminflt  45187  xlimpnfxnegmnf  45196  xlimmnf  45223  xlimpnf  45224  xlimmnfmpt  45225  xlimpnfmpt  45226  dfxlim2  45230  cncfshiftioo  45274  itgiccshift  45362  itgperiod  45363  fourierdlem42  45531  fourierdlem48  45536  fourierdlem81  45569  fourierdlem92  45580  fourierdlem96  45584  fourierdlem97  45585  fourierdlem98  45586  fourierdlem99  45587  fourierdlem105  45593  fourierdlem108  45596  fourierdlem110  45598  fourierdlem112  45600  fourierdlem113  45601  meaiunincf  45865  meaiuninc3v  45866  hoidmvval0  45969  ovnhoi  45985  ovolval5lem3  46036  ovolval5  46037  smfsup  46196  smfinflem  46199  smfinf  46200  fsetsnfo  46429  2reuimp0  46488  imaelsetpreimafv  46729  imasetpreimafvbijlemfo  46739  fundcmpsurinj  46743  fundcmpsurbijinj  46744  fmtnofac2lem  46902  2zlidl  47296  2zrngamgm  47301  2zrngagrp  47305  2zrngmmgm  47308  eenglngeehlnmlem1  47804