Theorem cbvrexvw 3217

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∃wex 1781   ∈ wcel 2114  ∃wrex 3062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-clel 2812  df-rex 3063

This theorem is referenced by:  cbvrex2vw  3221  reu7  3679  cbviunv  4982  disjiund  5077  reusv3  5342  xpdifid  6126  fliftfun  7260  funcnvuni  7876  fiunlem  7888  poseq  8101  soseq  8102  nneob  8585  coflton  8600  cofon1  8601  cofon2  8602  pssnn  9096  frfi  9188  finsschain  9262  marypha1lem  9339  supmo  9358  suplub2  9367  infmo  9403  ordtypelem3  9428  ordtypelem9  9434  wemaplem1  9454  brwdom3  9490  unwdomg  9492  cantnf  9605  ttrcltr  9628  trcl  9640  infxpenc2  9935  aceq2  10032  dfac5lem4  10039  dfac5lem4OLD  10041  kmlem9  10072  kmlem14  10077  fin23lem26  10238  fin1a2lem13  10325  axdc3lem3  10365  winainflem  10607  axgroth4  10746  suprlub  12111  supaddc  12114  supadd  12115  supmul1  12116  supmullem1  12117  supmullem2  12118  supmul  12119  ublbneg  12874  zsupss  12878  xrsupsslem  13250  xrinfmsslem  13251  rexanre  15300  rexuzre  15306  rexico  15307  caurcvg2  15631  caucvgb  15633  summolem2  15669  summo  15670  mertens  15842  prodmolem2  15891  prodmo  15892  odd2np1lem  16300  gcdcllem1  16459  prmdvdsncoprmbd  16688  pceu  16808  4sqlem12  16918  vdwlem10  16952  vdwlem13  16955  vdwnn  16960  drsdirfi  18262  grprida  18634  smndex1mgm  18869  smndex1mndlem  18871  dfgrp2  18929  dfgrp3lem  19005  cyccom  19169  gaorb  19273  psgnunilem3  19462  psgnunilem4  19463  psgneu  19472  pj1eu  19662  efgsfo  19705  cyggeninv  19849  cygabl  19857  pgpfac1lem5  20047  pgpfac1  20048  pgpfaclem2  20050  lss1d  20949  lspsneq  21112  lspsolvlem  21132  lbsextlem2  21149  cygznlem3  21559  mplcoe5lem  22027  pmatcollpw3fi1lem2  22762  ordtrest2lem  23178  cnprest  23264  1stcfb  23420  1stcelcls  23436  elpt  23547  fbssfi  23812  fgcl  23853  rnelfmlem  23927  fmfnfmlem3  23931  txflf  23981  alexsubb  24021  alexsubALTlem4  24025  isucn2  24253  icccmplem2  24799  ply1divex  26112  coeeu  26200  plydivex  26274  aannenlem2  26306  ulmcau  26373  ulmbdd  26376  dchrptlem2  27242  bposlem9  27269  2lgslem1b  27369  pntibndlem3  27569  pntlemi  27581  pntlemp  27587  pntleml  27588  pnt3  27589  nosupprefixmo  27678  noinfprefixmo  27679  nosupcbv  27680  nosupdm  27682  nosupfv  27684  nosupres  27685  nosupbnd1lem1  27686  nosupbnd1lem4  27689  noinfcbv  27695  noinfdm  27697  noinfbnd1lem4  27704  cofslts  27924  coinitslts  27925  addsval2  27969  addcuts  27984  addsunif  28008  norecdiv  28196  recsne0  28198  bdayn0sf1o  28376  dfnns2  28378  n0seo  28427  pw2recs  28444  bdayfinbndcbv  28472  bdayfinbndlem1  28473  bdayfinbndlem2  28474  recut  28500  readdscl  28505  legval  28666  legov  28667  legov2  28668  outpasch  28837  lnopp2hpgb  28845  colopp  28851  erclwwlksym  30106  erclwwlktr  30107  erclwwlknsym  30155  erclwwlkntr  30156  eleclclwwlkn  30161  hashecclwwlkn1  30162  umgrhashecclwwlk  30163  grpoidinvlem3  30592  ubthlem3  30958  norm1exi  31336  pjhthmo  31388  cdjreui  32518  cdj3i  32527  infxrge0glb  32853  mndlrinvb  33100  gsumwrd2dccatlem  33153  cyc3genpm  33228  isarchi3  33263  archiabl  33274  erler  33341  isdrng4  33371  1arithidomlem1  33610  1arithidom  33612  1arithufdlem2  33620  1arithufdlem3  33621  1arithufd  33623  fldext2chn  33888  constrconj  33905  constrextdg2lem  33908  constrextdg2  33909  constrfiss  33911  zarclsun  34030  ordtrest2NEWlem  34082  lmxrge0  34112  esumcvg  34246  esum2d  34253  eulerpartlems  34520  eulerpartlemgvv  34536  onvf1odlem2  35302  connpconn  35433  cvmlift2lem12  35512  cvmlift2lem13  35513  cvmlift3lem2  35518  cvmlift3lem7  35523  cvmlift3  35526  fmlasuc  35584  fmla1  35585  satffunlem1lem1  35600  satffunlem2lem1  35602  r1peuqusdeg1  35841  funtransport  36229  funray  36338  funline  36340  fnessref  36555  neibastop2  36559  dissneqlem  37670  dissneq  37671  pibt2  37747  ptrest  37954  poimirlem27  37982  poimirlem32  37987  ismblfin  37996  volsupnfl  38000  itg2addnclem  38006  unirep  38049  filbcmb  38075  sdclem1  38078  sdc  38079  fdc  38080  incsequz  38083  heibor1lem  38144  heiborlem10  38155  isgrpda  38290  isdrngo2  38293  prnc  38402  prtlem13  39328  prtlem15  39335  lshpsmreu  39569  lshpkrlem1  39570  lshpkrlem3  39572  pclfinN  40360  4atex  40536  dihglblem2N  41754  lcfl7N  41961  lcf1o  42011  supinf  42695  fimgmcyclem  42992  mzpcompact2lem  43197  eldioph3  43212  diophrex  43221  rexrabdioph  43240  eldioph4i  43258  aomclem8  43507  hbtlem2  43570  rngunsnply  43615  onsucrn  43717  iunrelexpuztr  44164  ntrclsneine0lem  44509  rexlimddvcbvw  44651  cpcoll2d  44704  mnuprdlem3  44719  dvconstbi  44779  expgrowth  44780  wessf1ornlem  45633  rnmptlb  45690  rnmptbdd  45692  rnmptbd2  45696  rnmptbd  45703  rexabsle  45865  uzub  45877  infrpgernmpt  45911  limcperiod  46076  limsupre  46087  limsupbnd1f  46132  climinf2  46153  climinfmpt  46161  limsupubuzmpt  46165  limsupmnf  46167  limsupre2  46171  limsupmnfuzlem  46172  limsupmnfuz  46173  limsupre2mpt  46176  limsupre3  46179  limsupre3mpt  46180  limsupre3uz  46182  limsupreuz  46183  limsupreuzmpt  46185  supcnvlimsup  46186  climuz  46190  lmbr3  46193  climrescn  46194  limsuplt2  46199  liminflelimsup  46222  limsupgt  46224  liminfreuz  46249  liminflt  46251  xlimpnfxnegmnf  46260  xlimmnf  46287  xlimpnf  46288  xlimmnfmpt  46289  xlimpnfmpt  46290  dfxlim2  46294  cncfshiftioo  46338  itgiccshift  46426  itgperiod  46427  fourierdlem42  46595  fourierdlem48  46600  fourierdlem81  46633  fourierdlem92  46644  fourierdlem96  46648  fourierdlem97  46649  fourierdlem98  46650  fourierdlem99  46651  fourierdlem105  46657  fourierdlem108  46660  fourierdlem110  46662  fourierdlem112  46664  fourierdlem113  46665  meaiunincf  46929  meaiuninc3v  46930  hoidmvval0  47033  ovnhoi  47049  ovolval5lem3  47100  ovolval5  47101  smfsup  47260  smfinflem  47263  smfinf  47264  nthrucw  47332  fsetsnfo  47513  2reuimp0  47574  nndivides2  47844  imaelsetpreimafv  47867  imasetpreimafvbijlemfo  47877  fundcmpsurinj  47881  fundcmpsurbijinj  47882  fmtnofac2lem  48043  2zlidl  48728  2zrngamgm  48733  2zrngagrp  48737  2zrngmmgm  48740  eenglngeehlnmlem1  49225  upciclem4  49656