Theorem cbvrexv 2766

Description: Change the bound variable of a restricted existential quantifier using implicit substitution. (Contributed by NM, 2-Jun-1998.)

Hypothesis

Ref	Expression
cbvralv.1	⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
cbvrexv	⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓)

Distinct variable groups:   𝑥,𝐴   𝑦,𝐴   𝜑,𝑦   𝜓,𝑥

Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦)

Proof of Theorem cbvrexv

Step	Hyp	Ref	Expression
1		nfv 1574	. 2 ⊢ Ⅎ𝑦𝜑
2		nfv 1574	. 2 ⊢ Ⅎ𝑥𝜓
3		cbvralv.1	. 2 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
4	1, 2, 3	cbvrex 2762	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ↔ wb 105  ∃wrex 2509

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-cleq 2222  df-clel 2225  df-nfc 2361  df-rex 2514

This theorem is referenced by:  cbvrex2v  2779  reu7  2998  reusv3  4548  funcnvuni  5386  fun11iun  5589  fvelimab  5683  fliftfun  5913  tfr1onlemaccex  6484  tfrcllemsucaccv  6490  tfrcllembxssdm  6492  tfrcllemaccex  6497  tfrcldm  6499  frecsuc  6543  nnaordex  6664  fimax2gtri  7051  supmoti  7148  suplub2ti  7156  fodjuomnilemdc  7299  fodjuomnilemres  7303  fodjuomni  7304  fodjumkvlemres  7314  fodjumkv  7315  nninfwlpoimlemginf  7331  nninfwlpoim  7334  nninfinfwlpo  7335  cardval3ex  7345  prarloclemlo  7669  prarloclem3  7672  cauappcvgprlemdisj  7826  cauappcvgprlemladdru  7831  cauappcvgprlemladdrl  7832  cauappcvgpr  7837  caucvgprlemdisj  7849  caucvgprlemcl  7851  caucvgprlemladdfu  7852  caucvgprlemladdrl  7853  caucvgpr  7857  caucvgprprlemell  7860  caucvgprprlemelu  7861  caucvgprprlemlol  7873  caucvgprprlemclphr  7880  caucvgprprlemexbt  7881  suplocexprlemmu  7893  suplocexpr  7900  suplocsrlem  7983  nntopi  8069  axcaucvglemres  8074  axpre-suploc  8077  suprzclex  9533  supinfneg  9778  infsupneg  9779  ublbneg  9796  suprzubdc  10443  exbtwnzlemstep  10454  exbtwnzlemshrink  10455  rebtwn2zlemstep  10459  rebtwn2zlemshrink  10460  hashunlem  11013  cvg1nlemres  11482  resqrexlemoverl  11518  resqrexlemsqa  11521  resqrexlemex  11522  rexanre  11717  rexico  11718  fimaxre2  11724  summodclem2  11879  summodc  11880  mertenslemub  12031  mertensabs  12034  odd2np1lem  12369  divalglemeunn  12418  divalglemeuneg  12420  bitsfzolem  12451  bezoutlemex  12508  ennnfoneleminc  12968  ennnfonelemex  12971  ennnfonelemhom  12972  ennnfonelemr  12980  ctinfom  12985  nninfdclemp1  13007  nninfdc  13010  cnptoprest  14898  dedekindeulemuub  15276  dedekindeulemub  15277  dedekindeulemloc  15278  dedekindeulemlub  15279  dedekindeulemlu  15280  dedekindicclemuub  15285  dedekindicclemub  15286  dedekindicclemloc  15287  dedekindicclemlub  15288  dedekindicclemlu  15289  ivthdich  15312  bj-nn0sucALT  16271  nconstwlpolem  16364  neapmkvlem  16366