Theorem cbvrexvw 3244

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 2176, ax-11 2192, ax-12 2213, 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 2846	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvralvw.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	1, 2	anbi12d 643	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑦 ∈ 𝐴 ∧ 𝜓)))
4	3	cbvexvw 2067	. 2 ⊢ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ 𝜓))
5		df-rex 3090	. 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
6		df-rex 3090	. 2 ⊢ (∃𝑦 ∈ 𝐴 𝜓 ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ 𝜓))
7	4, 5, 6	3bitr4i 306	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400  ∃wex 1809   ∈ wcel 2143  ∃wrex 3089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-clel 2838  df-rex 3090

This theorem is referenced by:  cbvrex2vw  3248  reu7  3695  cbviunv  5003  disjiund  5100  reusv3  5376  xpdifid  6165  xpdifcnvepel  6166  fliftfun  7310  funcnvuni  7925  fiunlem  7935  poseq  8150  soseq  8151  nneob  8638  coflton  8653  cofon1  8654  cofon2  8655  pssnn  9149  frfi  9241  finsschain  9312  marypha1lem  9389  supmo  9408  suplub2  9417  infmo  9453  ordtypelem3  9478  ordtypelem9  9484  wemaplem1  9504  brwdom3  9540  unwdomg  9542  cantnf  9658  ttrcltr  9681  trcl  9693  infxpenc2  10002  aceq2  10099  dfac5lem4  10106  kmlem9  10138  kmlem14  10143  fin23lem26  10304  fin1a2lem13  10391  axdc3lem3  10431  winainflem  10673  axgroth4  10812  suprlub  12174  supaddc  12177  supadd  12178  supmul1  12179  supmullem1  12180  supmullem2  12181  supmul  12182  ublbneg  12952  zsupss  12956  xrsupsslem  13328  xrinfmsslem  13329  rexanre  15394  rexuzre  15400  rexico  15401  caurcvg2  15725  caucvgb  15727  summolem2  15763  summo  15764  mertens  15936  prodmolem2  15985  prodmo  15986  odd2np1lem  16393  gcdcllem1  16552  prmdvdsncoprmbd  16781  pceu  16901  4sqlem12  17011  vdwlem10  17045  vdwlem13  17048  vdwnn  17053  drsdirfi  18356  grprida  18728  smndex1mgm  18964  smndex1mndlem  18966  dfgrp2  19024  dfgrp3lem  19099  cyccom  19269  gaorb  19372  psgnunilem3  19561  psgnunilem4  19562  psgneu  19571  pj1eu  19761  efgsfo  19804  cyggeninv  19948  cygabl  19956  pgpfac1lem5  20146  pgpfac1  20147  pgpfaclem2  20149  isdrng4  20839  isdrng3lem2  20852  lss1d  21084  lspsneq  21246  lspsolvlem  21266  lbsextlem2  21283  cygznlem3  21719  mplcoe5lem  22190  pmatcollpw3fi1lem2  22944  ordtrest2lem  23360  cnprest  23446  1stcfb  23602  1stcelcls  23618  elpt  23729  fbssfi  23994  fgcl  24035  rnelfmlem  24109  fmfnfmlem3  24113  txflf  24163  alexsubb  24203  alexsubALTlem4  24207  isucn2  24435  icccmplem2  24981  ply1divex  26294  coeeu  26382  plydivex  26458  aannenlem2  26492  ulmcau  26558  ulmbdd  26561  dchrptlem2  27429  bposlem9  27456  2lgslem1b  27556  pntibndlem3  27756  pntlemi  27768  pntlemp  27774  pntleml  27775  pnt3  27776  nosupprefixmo  27864  noinfprefixmo  27865  nosupcbv  27866  nosupdm  27868  nosupfv  27870  nosupres  27871  nosupbnd1lem1  27872  nosupbnd1lem4  27875  noinfcbv  27881  noinfdm  27883  noinfbnd1lem4  27890  cofslts  28111  coinitslts  28112  addsval2  28156  addcuts  28171  addsunif  28195  norecdiv  28383  recsne0  28385  bdayn0sf1o  28563  dfnns2  28565  n0seo  28614  pw2recs  28631  bdayfinbndcbv  28659  bdayfinbndlem1  28660  bdayfinbndlem2  28661  recut  28687  readdscl  28692  legval  28853  legov  28854  legov2  28855  outpasch  29037  lnopp2hpgb  29045  colopp  29051  elplngid  29064  lnincplng  29066  plngcp  29068  plngrot  29072  nhpmirhp  29080  lnperpexs  29114  ragraghl  29149  prlnghpg  29196  prlngmo  29204  tgaltai  29217  erclwwlksym  30372  erclwwlktr  30373  erclwwlknsym  30421  erclwwlkntr  30422  eleclclwwlkn  30427  hashecclwwlkn1  30428  umgrhashecclwwlk  30429  grpoidinvlem3  30858  ubthlem3  31224  norm1exi  31602  pjhthmo  31654  cdjreui  32784  cdj3i  32793  infxrge0glb  33110  mndlrinvb  33345  gsumwrd2dccatlem  33397  cyc3genpm  33472  isarchi3  33507  archiabl  33518  erler  33585  rlocisunit  33596  1arithidomlem1  33825  1arithidom  33827  1arithufdlem2  33835  1arithufdlem3  33836  1arithufd  33838  fldext2chn  34118  constrconj  34135  constrextdg2lem  34138  constrextdg2  34139  constrfiss  34141  zarclsun  34260  ordtrest2NEWlem  34312  lmxrge0  34342  esumcvg  34476  esum2d  34483  eulerpartlems  34750  eulerpartlemgvv  34766  onvf1odlem2  35588  connpconn  35727  cvmlift2lem12  35806  cvmlift2lem13  35807  cvmlift3lem2  35812  cvmlift3lem7  35817  cvmlift3  35820  fmlasuc  35878  fmla1  35879  satffunlem1lem1  35894  satffunlem2lem1  35896  r1peuqusdeg1  36135  funtransport  36523  funray  36632  funline  36634  fnessref  36868  neibastop2  36872  dissneqlem  37986  dissneq  37987  pibt2  38063  ptrest  38270  poimirlem27  38298  poimirlem32  38303  ismblfin  38312  volsupnfl  38316  itg2addnclem  38322  unirep  38365  filbcmb  38391  sdclem1  38394  sdc  38395  fdc  38396  incsequz  38399  heibor1lem  38460  heiborlem10  38471  isgrpda  38606  isdrngo2  38609  prnc  38718  prtlem13  39642  prtlem15  39649  lshpsmreu  39883  lshpkrlem1  39884  lshpkrlem3  39886  pclfinN  40674  4atex  40850  dihglblem2N  42068  lcfl7N  42275  lcf1o  42325  supinf  43010  fimgmcyclem  43301  mzpcompact2lem  43482  eldioph3  43497  diophrex  43506  rexrabdioph  43521  eldioph4i  43539  aomclem8  43788  hbtlem2  43851  rngunsnply  43896  onsucrn  43998  iunrelexpuztr  44445  ntrclsneine0lem  44790  rexlimddvcbvw  44930  cpcoll2d  44969  mnuprdlem3  44984  dvconstbi  45044  expgrowth  45045  wessf1ornlem  45903  rnmptlb  45958  rnmptbdd  45960  rnmptbd2  45964  rnmptbd  45971  rexabsle  46133  uzub  46145  infrpgernmpt  46179  limcperiod  46344  limsupre  46355  limsupbnd1f  46400  climinf2  46421  climinfmpt  46429  limsupubuzmpt  46433  limsupmnf  46435  limsupre2  46439  limsupmnfuzlem  46440  limsupmnfuz  46441  limsupre2mpt  46444  limsupre3  46447  limsupre3mpt  46448  limsupre3uz  46450  limsupreuz  46451  limsupreuzmpt  46453  supcnvlimsup  46454  climuz  46458  lmbr3  46461  climrescn  46462  limsuplt2  46467  liminflelimsup  46490  limsupgt  46492  liminfreuz  46517  liminflt  46519  xlimpnfxnegmnf  46528  xlimmnf  46555  xlimpnf  46556  xlimmnfmpt  46557  xlimpnfmpt  46558  dfxlim2  46562  cncfshiftioo  46606  itgiccshift  46694  itgperiod  46695  fourierdlem42  46863  fourierdlem48  46868  fourierdlem81  46901  fourierdlem92  46912  fourierdlem96  46916  fourierdlem97  46917  fourierdlem98  46918  fourierdlem99  46919  fourierdlem105  46925  fourierdlem108  46928  fourierdlem110  46930  fourierdlem112  46932  fourierdlem113  46933  meaiunincf  47197  meaiuninc3v  47198  hoidmvval0  47301  ovnhoi  47317  ovolval5lem3  47368  ovolval5  47369  smfsup  47528  smfinflem  47531  smfinf  47532  fsetsnfo  47790  2reuimp0  47851  nndivides2  48121  imaelsetpreimafv  48144  imasetpreimafvbijlemfo  48154  fundcmpsurinj  48158  fundcmpsurbijinj  48159  fmtnofac2lem  48320  2zlidl  49005  2zrngamgm  49010  2zrngagrp  49014  2zrngmmgm  49017  eenglngeehlnmlem1  49517  upciclem4  49947