Theorem cbvrexvw 3235

Description: Change the bound variable of a restricted existential quantifier using implicit substitution. Version of cbvrexv 3361 with a disjoint variable condition, which does not require ax-10 2137, ax-11 2154, ax-12 2171, ax-13 2371. (Contributed by NM, 2-Jun-1998.) Avoid ax-13 2371. (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 2816	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvralvw.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	1, 2	anbi12d 631	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑦 ∈ 𝐴 ∧ 𝜓)))
4	3	cbvexvw 2040	. 2 ⊢ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ 𝜓))
5		df-rex 3071	. 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
6		df-rex 3071	. 2 ⊢ (∃𝑦 ∈ 𝐴 𝜓 ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ 𝜓))
7	4, 5, 6	3bitr4i 302	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396  ∃wex 1781   ∈ wcel 2106  ∃wrex 3070

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 1913  ax-6 1971  ax-7 2011  ax-8 2108

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-clel 2810  df-rex 3071

This theorem is referenced by:  cbvrex2vw  3239  reu7  3728  disjiund  5138  reusv3  5403  xpdifid  6167  fliftfun  7311  funcnvuni  7924  fiunlem  7930  poseq  8146  soseq  8147  nneob  8657  coflton  8672  cofon1  8673  cofon2  8674  pssnn  9170  pssnnOLD  9267  frfi  9290  finsschain  9361  marypha1lem  9430  supmo  9449  suplub2  9458  infmo  9492  ordtypelem3  9517  ordtypelem9  9523  wemaplem1  9543  brwdom3  9579  unwdomg  9581  cantnf  9690  ttrcltr  9713  trcl  9725  infxpenc2  10019  aceq2  10116  dfac5lem4  10123  kmlem9  10155  kmlem14  10160  fin23lem26  10322  fin1a2lem13  10409  axdc3lem3  10449  winainflem  10690  axgroth4  10829  suprlub  12180  supaddc  12183  supadd  12184  supmul1  12185  supmullem1  12186  supmullem2  12187  supmul  12188  ublbneg  12919  zsupss  12923  xrsupsslem  13288  xrinfmsslem  13289  rexanre  15295  rexuzre  15301  rexico  15302  caurcvg2  15626  caucvgb  15628  summolem2  15664  summo  15665  mertens  15834  prodmolem2  15881  prodmo  15882  odd2np1lem  16285  gcdcllem1  16442  prmdvdsncoprmbd  16665  pceu  16781  4sqlem12  16891  vdwlem10  16925  vdwlem13  16928  vdwnn  16933  drsdirfi  18260  grprida  18596  smndex1mgm  18790  smndex1mndlem  18792  dfgrp2  18849  dfgrp3lem  18923  cyccom  19082  gaorb  19173  psgnunilem3  19366  psgnunilem4  19367  psgneu  19376  pj1eu  19566  efgsfo  19609  cyggeninv  19753  cygabl  19761  pgpfac1lem5  19951  pgpfac1  19952  pgpfaclem2  19954  lss1d  20579  lspsneq  20741  lspsolvlem  20761  lbsextlem2  20778  cygznlem3  21131  mplcoe5lem  21600  pmatcollpw3fi1lem2  22296  ordtrest2lem  22714  cnprest  22800  1stcfb  22956  1stcelcls  22972  elpt  23083  fbssfi  23348  fgcl  23389  rnelfmlem  23463  fmfnfmlem3  23467  txflf  23517  alexsubb  23557  alexsubALTlem4  23561  isucn2  23791  icccmplem2  24346  ply1divex  25661  coeeu  25746  plydivex  25817  aannenlem2  25849  ulmcau  25914  ulmbdd  25917  dchrptlem2  26775  bposlem9  26802  2lgslem1b  26902  pntibndlem3  27102  pntlemi  27114  pntlemp  27120  pntleml  27121  pnt3  27122  nosupprefixmo  27210  noinfprefixmo  27211  nosupcbv  27212  nosupdm  27214  nosupfv  27216  nosupres  27217  nosupbnd1lem1  27218  nosupbnd1lem4  27221  noinfcbv  27227  noinfdm  27229  noinfbnd1lem4  27236  cofsslt  27414  coinitsslt  27415  addsval2  27456  addscut  27471  addsunif  27495  norecdiv  27648  legval  27873  legov  27874  legov2  27875  outpasch  28044  lnopp2hpgb  28052  colopp  28058  erclwwlksym  29312  erclwwlktr  29313  erclwwlknsym  29361  erclwwlkntr  29362  eleclclwwlkn  29367  hashecclwwlkn1  29368  umgrhashecclwwlk  29369  grpoidinvlem3  29797  ubthlem3  30163  norm1exi  30541  pjhthmo  30593  cdjreui  31723  cdj3i  31732  infxrge0glb  32016  cyc3genpm  32352  isarchi3  32374  archiabl  32385  isdrng4  32436  zarclsun  32919  ordtrest2NEWlem  32971  lmxrge0  33001  esumcvg  33153  esum2d  33160  eulerpartlems  33428  eulerpartlemgvv  33444  connpconn  34295  cvmlift2lem12  34374  cvmlift2lem13  34375  cvmlift3lem2  34380  cvmlift3lem7  34385  cvmlift3  34388  fmlasuc  34446  fmla1  34447  satffunlem1lem1  34462  satffunlem2lem1  34464  funtransport  35072  funray  35181  funline  35183  fnessref  35328  neibastop2  35332  dissneqlem  36307  dissneq  36308  pibt2  36384  ptrest  36573  poimirlem27  36601  poimirlem32  36606  ismblfin  36615  volsupnfl  36619  itg2addnclem  36625  unirep  36668  filbcmb  36694  sdclem1  36697  sdc  36698  fdc  36699  incsequz  36702  heibor1lem  36763  heiborlem10  36774  isgrpda  36909  isdrngo2  36912  prnc  37021  prtlem13  37824  prtlem15  37831  lshpsmreu  38065  lshpkrlem1  38066  lshpkrlem3  38068  pclfinN  38857  4atex  39033  dihglblem2N  40251  lcfl7N  40458  lcf1o  40508  mzpcompact2lem  41571  eldioph3  41586  diophrex  41595  rexrabdioph  41614  eldioph4i  41632  aomclem8  41885  hbtlem2  41948  rngunsnply  41997  onsucrn  42103  iunrelexpuztr  42552  ntrclsneine0lem  42897  rexlimddvcbvw  43040  cpcoll2d  43100  mnuprdlem3  43115  dvconstbi  43175  expgrowth  43176  wessf1ornlem  43963  rnmptlb  44026  rnmptbdd  44028  rnmptbd2  44032  rnmptbd  44039  rexabsle  44208  uzub  44220  infrpgernmpt  44254  limcperiod  44423  limsupre  44436  limsupbnd1f  44481  climinf2  44502  climinfmpt  44510  limsupubuzmpt  44514  limsupmnf  44516  limsupre2  44520  limsupmnfuzlem  44521  limsupmnfuz  44522  limsupre2mpt  44525  limsupre3  44528  limsupre3mpt  44529  limsupre3uz  44531  limsupreuz  44532  limsupreuzmpt  44534  supcnvlimsup  44535  climuz  44539  lmbr3  44542  climrescn  44543  limsuplt2  44548  liminflelimsup  44571  limsupgt  44573  liminfreuz  44598  liminflt  44600  xlimpnfxnegmnf  44609  xlimmnf  44636  xlimpnf  44637  xlimmnfmpt  44638  xlimpnfmpt  44639  dfxlim2  44643  cncfshiftioo  44687  itgiccshift  44775  itgperiod  44776  fourierdlem42  44944  fourierdlem48  44949  fourierdlem81  44982  fourierdlem92  44993  fourierdlem96  44997  fourierdlem97  44998  fourierdlem98  44999  fourierdlem99  45000  fourierdlem105  45006  fourierdlem108  45009  fourierdlem110  45011  fourierdlem112  45013  fourierdlem113  45014  meaiunincf  45278  meaiuninc3v  45279  hoidmvval0  45382  ovnhoi  45398  ovolval5lem3  45449  ovolval5  45450  smfsup  45609  smfinflem  45612  smfinf  45613  fsetsnfo  45842  2reuimp0  45901  imaelsetpreimafv  46142  imasetpreimafvbijlemfo  46152  fundcmpsurinj  46156  fundcmpsurbijinj  46157  fmtnofac2lem  46315  2zlidl  46911  2zrngamgm  46916  2zrngagrp  46920  2zrngmmgm  46923  eenglngeehlnmlem1  47501