Theorem cbvrexv 2778

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 1577	. 2 ⊢ Ⅎ𝑦𝜑
2		nfv 1577	. 2 ⊢ Ⅎ𝑥𝜓
3		cbvralv.1	. 2 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
4	1, 2, 3	cbvrex 2774	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓)

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

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-cleq 2225  df-clel 2228  df-nfc 2373  df-rex 2526

This theorem is referenced by:  cbvrex2v  2791  reu7  3011  reusv3  4580  funcnvuni  5424  fun11iun  5634  fvelimab  5732  fliftfun  5968  tfr1onlemaccex  6578  tfrcllemsucaccv  6584  tfrcllembxssdm  6586  tfrcllemaccex  6591  tfrcldm  6593  frecsuc  6637  nnaordex  6760  fimax2gtri  7158  supmoti  7283  suplub2ti  7291  fodjuomnilemdc  7434  fodjuomnilemres  7438  fodjuomni  7439  fodjumkvlemres  7449  fodjumkv  7450  nninfwlpoimlemginf  7466  nninfwlpoim  7469  nninfinfwlpo  7470  cardval3ex  7480  prarloclemlo  7808  prarloclem3  7811  cauappcvgprlemdisj  7965  cauappcvgprlemladdru  7970  cauappcvgprlemladdrl  7971  cauappcvgpr  7976  caucvgprlemdisj  7988  caucvgprlemcl  7990  caucvgprlemladdfu  7991  caucvgprlemladdrl  7992  caucvgpr  7996  caucvgprprlemell  7999  caucvgprprlemelu  8000  caucvgprprlemlol  8012  caucvgprprlemclphr  8019  caucvgprprlemexbt  8020  suplocexprlemmu  8032  suplocexpr  8039  suplocsrlem  8122  nntopi  8208  axcaucvglemres  8213  axpre-suploc  8216  suprzclex  9675  supinfneg  9926  infsupneg  9927  ublbneg  9944  suprzubdc  10595  exbtwnzlemstep  10606  exbtwnzlemshrink  10607  rebtwn2zlemstep  10611  rebtwn2zlemshrink  10612  hashunlem  11166  cvg1nlemres  11666  resqrexlemoverl  11702  resqrexlemsqa  11705  resqrexlemex  11706  rexanre  11901  rexico  11902  fimaxre2  11908  summodclem2  12064  summodc  12065  mertenslemub  12216  mertensabs  12219  odd2np1lem  12554  divalglemeunn  12603  divalglemeuneg  12605  bitsfzolem  12636  bezoutlemex  12693  ennnfoneleminc  13154  ennnfonelemex  13157  ennnfonelemhom  13158  ennnfonelemr  13166  ctinfom  13171  nninfdclemp1  13193  nninfdc  13196  cnptoprest  15096  dedekindeulemuub  15474  dedekindeulemub  15475  dedekindeulemloc  15476  dedekindeulemlub  15477  dedekindeulemlu  15478  dedekindicclemuub  15483  dedekindicclemub  15484  dedekindicclemloc  15485  dedekindicclemlub  15486  dedekindicclemlu  15487  ivthdich  15510  bj-nn0sucALT  16740  nconstwlpolem  16842  neapmkvlem  16844