Theorem cbvrexvw 3245

Description: Change the bound variable of a restricted existential quantifier using implicit substitution. Version of cbvrexv 3354 with a disjoint variable condition, which does not require ax-10 2180, ax-11 2197, ax-12 2216, ax-13 2404. (Contributed by NM, 2-Jun-1998.) Avoid ax-13 2404. (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 2847	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvralvw.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	1, 2	anbi12d 644	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑦 ∈ 𝐴 ∧ 𝜓)))
4	3	cbvexvw 2072	. 2 ⊢ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ 𝜓))
5		df-rex 3091	. 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
6		df-rex 3091	. 2 ⊢ (∃𝑦 ∈ 𝐴 𝜓 ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ 𝜓))
7	4, 5, 6	3bitr4i 306	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401  ∃wex 1812   ∈ wcel 2147  ∃wrex 3090

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-clel 2839  df-rex 3091

This theorem is used by:  cbvrex2vw  3249  reu7  3693  cbviunv  5002  disjiund  5099  reusv3  5374  xpdifid  6177  xpdifcnvepel  6178  fliftfun  7351  funcnvuni  7978  fiunlem  7988  poseq  8212  soseq  8213  nneob  8703  coflton  8718  cofon1  8719  cofon2  8720  pssnn  9222  frfi  9314  finsschain  9386  marypha1lem  9462  supmo  9481  suplub2  9490  infmo  9526  ordtypelem3  9551  ordtypelem9  9557  wemaplem1  9577  brwdom3  9613  unwdomg  9615  cantnf  9731  ttrcltr  9754  trcl  9766  infxpenc2  10140  aceq2  10237  dfac5lem4  10244  kmlem9  10276  kmlem14  10281  fin23lem26  10442  fin1a2lem13  10529  axdc3lem3  10569  winainflem  10817  axgroth4  10956  suprlub  12321  supaddc  12324  supadd  12325  supmul1  12326  supmullem1  12327  supmullem2  12328  supmul  12329  ublbneg  13100  zsupss  13104  xrsupsslem  13477  xrinfmsslem  13478  rexanre  15558  rexuzre  15564  rexico  15565  caurcvg2  15889  caucvgb  15891  summolem2  15926  summo  15927  mertens  16099  prodmolem2  16146  prodmo  16147  odd2np1lem  16554  gcdcllem1  16713  prmdvdsncoprmbd  16947  pceu  17068  4sqlem12  17178  vdwlem10  17212  vdwlem13  17215  vdwnn  17220  drsdirfi  18529  0gisid  18898  grprida  18906  smndex1mgm  19156  smndex1mndlem  19158  dfgrp2  19223  dfgrp3lem  19298  cyccom  19468  gaorb  19572  psgnunilem3  19761  psgnunilem4  19762  psgneu  19771  pj1eu  19961  efgsfo  20004  cyggeninv  20148  cygabl  20156  pgpfac1lem5  20346  pgpfac1  20347  pgpfaclem2  20349  isdrng4  21043  isdrng3lem2  21057  lss1d  21289  lspsneq  21451  lspsolvlem  21471  lbsextlem2  21488  cygznlem3  21930  mplcoe5lem  22403  pmatcollpw3fi1lem2  23160  ordtrest2lem  23576  cnprest  23662  1stcfb  23818  1stcelcls  23835  elpt  23946  fbssfi  24211  fgcl  24252  rnelfmlem  24326  fmfnfmlem3  24330  txflf  24380  alexsubb  24420  alexsubALTlem4  24424  isucn2  24652  icccmplem2  25198  ply1divex  26510  coeeu  26599  plydivex  26673  rngunsnply  26693  aannenlem2  26713  ulmcau  26779  ulmbdd  26782  dchrptlem2  27649  bposlem9  27676  2lgslem1b  27776  pntibndlem3  27976  pntlemi  27988  pntlemp  27994  pntleml  27995  pnt3  27996  nosupprefixmo  28114  noinfprefixmo  28115  nosupcbv  28116  nosupdm  28118  nosupfv  28120  nosupres  28121  nosupbnd1lem1  28122  nosupbnd1lem4  28125  noinfcbv  28131  noinfdm  28133  noinfbnd1lem4  28140  cofslts  28361  coinitslts  28362  addsval2  28406  addcuts  28421  addsunif  28445  norecdiv  28633  recsne0  28635  bdayn0sf1o  28813  dfnns2  28815  n0seo  28864  pw2recs  28881  bdayfinbndcbv  28909  bdayfinbndlem1  28910  bdayfinbndlem2  28911  recut  28937  readdscl  28942  legval  29104  legov  29105  legov2  29106  outpasch  29290  lnopp2hpgb  29298  colopp  29304  elplngid  29317  lnincplng  29319  plngcp  29321  plngrot  29325  nhpmirhp  29333  lnperpexs  29367  ragraghl  29403  tgaaddcpbllem2  29407  tgaaddcpbllem3  29408  tgaaddcpbl2  29410  angmgmaddeu1  29436  angmgmaddcl  29448  prlnghpg  29481  prlngmo  29489  tgaltai  29502  erclwwlksym  30669  erclwwlktr  30670  erclwwlknsym  30718  erclwwlkntr  30719  eleclclwwlkn  30724  hashecclwwlkn1  30725  umgrhashecclwwlk  30726  grpoidinvlem3  31165  ubthlem3  31531  norm1exi  31909  pjhthmo  31961  cdjreui  33091  cdj3i  33100  infxrge0glb  33453  mndlrinvb  33685  gsumwrd2dccatlem  33737  cyc3genpm  33812  isarchi3  33847  archiabl  33858  erler  33925  rlocisunit  33936  1arithidomlem1  34171  1arithidom  34173  1arithufdlem2  34181  1arithufdlem3  34182  1arithufd  34184  fldext2chn  34471  constrconj  34488  constrextdg2lem  34491  constrextdg2  34492  constrfiss  34494  zarclsun  34613  ordtrest2NEWlem  34665  lmxrge0  34695  esumcvg  34829  esum2d  34836  eulerpartlems  35103  eulerpartlemgvv  35119  onvf1odlem2  36073  connpconn  36208  cvmlift2lem12  36287  cvmlift2lem13  36288  cvmlift3lem2  36293  cvmlift3lem7  36298  cvmlift3  36301  fmlasuc  36359  fmla1  36360  satffunlem1lem1  36375  satffunlem2lem1  36377  r1peuqusdeg1  36616  mirimanofffr  36670  funtransport  37011  funray  37120  funline  37122  fnessref  37360  neibastop2  37364  dissneqlem  38531  dissneq  38532  pibt2  38608  ptrest  38805  poimirlem27  38833  poimirlem32  38838  ismblfin  38847  volsupnfl  38851  itg2addnclem  38857  unirep  38916  filbcmb  38940  sdclem1  38943  sdc  38944  fdc  38945  incsequz  38948  heibor1lem  39009  heiborlem10  39020  isgrpda  39155  isdrngo2  39158  prnc  39267  prtlem13  40191  prtlem15  40198  lshpsmreu  40432  lshpkrlem1  40433  lshpkrlem3  40435  pclfinN  41223  4atex  41399  dihglblem2N  42617  lcfl7N  42824  lcf1o  42874  supinf  43560  fimgmcyclem  43863  mzpcompact2lem  44028  eldioph3  44043  diophrex  44052  rexrabdioph  44067  eldioph4i  44085  aomclem8  44329  hbtlem2  44391  onsucrn  44534  iunrelexpuztr  44980  ntrclsneine0lem  45325  rexlimddvcbvw  45465  cpcoll2d  45504  mnuprdlem3  45519  dvconstbi  45579  expgrowth  45580  wessf1ornlem  46473  rnmptlb  46528  rnmptbdd  46530  rnmptbd2  46534  rnmptbd  46541  rexabsle  46702  uzub  46714  infrpgernmpt  46748  limcperiod  46913  limsupre  46924  limsupbnd1f  46969  climinf2  46990  climinfmpt  46998  limsupubuzmpt  47002  limsupmnf  47004  limsupre2  47008  limsupmnfuzlem  47009  limsupmnfuz  47010  limsupre2mpt  47013  limsupre3  47016  limsupre3mpt  47017  limsupre3uz  47019  limsupreuz  47020  limsupreuzmpt  47022  supcnvlimsup  47023  climuz  47027  lmbr3  47030  climrescn  47031  limsuplt2  47036  liminflelimsup  47059  limsupgt  47061  liminfreuz  47086  liminflt  47088  xlimpnfxnegmnf  47097  xlimmnf  47124  xlimpnf  47125  xlimmnfmpt  47126  xlimpnfmpt  47127  dfxlim2  47131  cncfshiftioo  47175  itgiccshift  47263  itgperiod  47264  fourierdlem42  47432  fourierdlem48  47437  fourierdlem81  47470  fourierdlem92  47481  fourierdlem96  47485  fourierdlem97  47486  fourierdlem98  47487  fourierdlem99  47488  fourierdlem105  47494  fourierdlem108  47497  fourierdlem110  47499  fourierdlem112  47501  fourierdlem113  47502  meaiunincf  47766  meaiuninc3v  47767  hoidmvval0  47870  ovnhoi  47886  ovolval5lem3  47937  ovolval5  47938  smfsup  48097  smfinflem  48100  smfinf  48101  fsetsnfo  48396  2reuimp0  48458  nndivides2  48727  imaelsetpreimafv  48750  imasetpreimafvbijlemfo  48760  fundcmpsurinj  48764  fundcmpsurbijinj  48765  fmtnofac2lem  48926  2zlidl  49610  2zrngamgm  49615  2zrngagrp  49619  2zrngmmgm  49622  eenglngeehlnmlem1  50181  upciclem4  50616