Theorem cbvrexvw 3216

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∃wex 1779   ∈ wcel 2109  ∃wrex 3053

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-clel 2803  df-rex 3054

This theorem is referenced by:  cbvrex2vw  3220  reu7  3703  cbviunv  5004  disjiund  5098  reusv3  5360  xpdifid  6141  fliftfun  7287  funcnvuni  7908  fiunlem  7920  poseq  8137  soseq  8138  nneob  8620  coflton  8635  cofon1  8636  cofon2  8637  pssnn  9132  frfi  9232  finsschain  9310  marypha1lem  9384  supmo  9403  suplub2  9412  infmo  9448  ordtypelem3  9473  ordtypelem9  9479  wemaplem1  9499  brwdom3  9535  unwdomg  9537  cantnf  9646  ttrcltr  9669  trcl  9681  infxpenc2  9975  aceq2  10072  dfac5lem4  10079  dfac5lem4OLD  10081  kmlem9  10112  kmlem14  10117  fin23lem26  10278  fin1a2lem13  10365  axdc3lem3  10405  winainflem  10646  axgroth4  10785  suprlub  12147  supaddc  12150  supadd  12151  supmul1  12152  supmullem1  12153  supmullem2  12154  supmul  12155  ublbneg  12892  zsupss  12896  xrsupsslem  13267  xrinfmsslem  13268  rexanre  15313  rexuzre  15319  rexico  15320  caurcvg2  15644  caucvgb  15646  summolem2  15682  summo  15683  mertens  15852  prodmolem2  15901  prodmo  15902  odd2np1lem  16310  gcdcllem1  16469  prmdvdsncoprmbd  16697  pceu  16817  4sqlem12  16927  vdwlem10  16961  vdwlem13  16964  vdwnn  16969  drsdirfi  18266  grprida  18602  smndex1mgm  18834  smndex1mndlem  18836  dfgrp2  18894  dfgrp3lem  18970  cyccom  19135  gaorb  19239  psgnunilem3  19426  psgnunilem4  19427  psgneu  19436  pj1eu  19626  efgsfo  19669  cyggeninv  19813  cygabl  19821  pgpfac1lem5  20011  pgpfac1  20012  pgpfaclem2  20014  lss1d  20869  lspsneq  21032  lspsolvlem  21052  lbsextlem2  21069  cygznlem3  21479  mplcoe5lem  21946  pmatcollpw3fi1lem2  22674  ordtrest2lem  23090  cnprest  23176  1stcfb  23332  1stcelcls  23348  elpt  23459  fbssfi  23724  fgcl  23765  rnelfmlem  23839  fmfnfmlem3  23843  txflf  23893  alexsubb  23933  alexsubALTlem4  23937  isucn2  24166  icccmplem2  24712  ply1divex  26042  coeeu  26130  plydivex  26205  aannenlem2  26237  ulmcau  26304  ulmbdd  26307  dchrptlem2  27176  bposlem9  27203  2lgslem1b  27303  pntibndlem3  27503  pntlemi  27515  pntlemp  27521  pntleml  27522  pnt3  27523  nosupprefixmo  27612  noinfprefixmo  27613  nosupcbv  27614  nosupdm  27616  nosupfv  27618  nosupres  27619  nosupbnd1lem1  27620  nosupbnd1lem4  27623  noinfcbv  27629  noinfdm  27631  noinfbnd1lem4  27638  cofsslt  27826  coinitsslt  27827  addsval2  27870  addscut  27885  addsunif  27909  norecdiv  28093  recsne0  28095  bdayn0sf1o  28259  dfnns2  28261  n0seo  28307  pw2recs  28323  recut  28347  readdscl  28350  legval  28511  legov  28512  legov2  28513  outpasch  28682  lnopp2hpgb  28690  colopp  28696  erclwwlksym  29950  erclwwlktr  29951  erclwwlknsym  29999  erclwwlkntr  30000  eleclclwwlkn  30005  hashecclwwlkn1  30006  umgrhashecclwwlk  30007  grpoidinvlem3  30435  ubthlem3  30801  norm1exi  31179  pjhthmo  31231  cdjreui  32361  cdj3i  32370  infxrge0glb  32688  mndlrinvb  32966  gsumwrd2dccatlem  33006  cyc3genpm  33109  isarchi3  33141  archiabl  33152  erler  33216  isdrng4  33245  1arithidomlem1  33506  1arithidom  33508  1arithufdlem2  33516  1arithufdlem3  33517  1arithufd  33519  fldext2chn  33718  constrconj  33735  constrextdg2lem  33738  constrextdg2  33739  constrfiss  33741  zarclsun  33860  ordtrest2NEWlem  33912  lmxrge0  33942  esumcvg  34076  esum2d  34083  eulerpartlems  34351  eulerpartlemgvv  34367  onvf1odlem2  35091  connpconn  35222  cvmlift2lem12  35301  cvmlift2lem13  35302  cvmlift3lem2  35307  cvmlift3lem7  35312  cvmlift3  35315  fmlasuc  35373  fmla1  35374  satffunlem1lem1  35389  satffunlem2lem1  35391  r1peuqusdeg1  35630  funtransport  36019  funray  36128  funline  36130  fnessref  36345  neibastop2  36349  dissneqlem  37328  dissneq  37329  pibt2  37405  ptrest  37613  poimirlem27  37641  poimirlem32  37646  ismblfin  37655  volsupnfl  37659  itg2addnclem  37665  unirep  37708  filbcmb  37734  sdclem1  37737  sdc  37738  fdc  37739  incsequz  37742  heibor1lem  37803  heiborlem10  37814  isgrpda  37949  isdrngo2  37952  prnc  38061  prtlem13  38861  prtlem15  38868  lshpsmreu  39102  lshpkrlem1  39103  lshpkrlem3  39105  pclfinN  39894  4atex  40070  dihglblem2N  41288  lcfl7N  41495  lcf1o  41545  supinf  42230  fimgmcyclem  42521  mzpcompact2lem  42739  eldioph3  42754  diophrex  42763  rexrabdioph  42782  eldioph4i  42800  aomclem8  43050  hbtlem2  43113  rngunsnply  43158  onsucrn  43260  iunrelexpuztr  43708  ntrclsneine0lem  44053  rexlimddvcbvw  44195  cpcoll2d  44248  mnuprdlem3  44263  dvconstbi  44323  expgrowth  44324  wessf1ornlem  45179  rnmptlb  45237  rnmptbdd  45239  rnmptbd2  45243  rnmptbd  45250  rexabsle  45415  uzub  45427  infrpgernmpt  45461  limcperiod  45626  limsupre  45639  limsupbnd1f  45684  climinf2  45705  climinfmpt  45713  limsupubuzmpt  45717  limsupmnf  45719  limsupre2  45723  limsupmnfuzlem  45724  limsupmnfuz  45725  limsupre2mpt  45728  limsupre3  45731  limsupre3mpt  45732  limsupre3uz  45734  limsupreuz  45735  limsupreuzmpt  45737  supcnvlimsup  45738  climuz  45742  lmbr3  45745  climrescn  45746  limsuplt2  45751  liminflelimsup  45774  limsupgt  45776  liminfreuz  45801  liminflt  45803  xlimpnfxnegmnf  45812  xlimmnf  45839  xlimpnf  45840  xlimmnfmpt  45841  xlimpnfmpt  45842  dfxlim2  45846  cncfshiftioo  45890  itgiccshift  45978  itgperiod  45979  fourierdlem42  46147  fourierdlem48  46152  fourierdlem81  46185  fourierdlem92  46196  fourierdlem96  46200  fourierdlem97  46201  fourierdlem98  46202  fourierdlem99  46203  fourierdlem105  46209  fourierdlem108  46212  fourierdlem110  46214  fourierdlem112  46216  fourierdlem113  46217  meaiunincf  46481  meaiuninc3v  46482  hoidmvval0  46585  ovnhoi  46601  ovolval5lem3  46652  ovolval5  46653  smfsup  46812  smfinflem  46815  smfinf  46816  fsetsnfo  47054  2reuimp0  47115  imaelsetpreimafv  47396  imasetpreimafvbijlemfo  47406  fundcmpsurinj  47410  fundcmpsurbijinj  47411  fmtnofac2lem  47569  2zlidl  48228  2zrngamgm  48233  2zrngagrp  48237  2zrngmmgm  48240  eenglngeehlnmlem1  48726  upciclem4  49158