Theorem cbvrexv 2781

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 2777	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓)

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

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 2216

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-cleq 2227  df-clel 2230  df-nfc 2375  df-rex 2528

This theorem is referenced by:  cbvrex2v  2794  reu7  3015  reusv3  4586  funcnvuni  5430  fun11iun  5640  fvelimab  5738  fliftfun  5975  tfr1onlemaccex  6592  tfrcllemsucaccv  6598  tfrcllembxssdm  6600  tfrcllemaccex  6605  tfrcldm  6607  frecsuc  6651  nnaordex  6774  fimax2gtri  7172  supmoti  7297  suplub2ti  7305  fodjuomnilemdc  7448  fodjuomnilemres  7452  fodjuomni  7453  fodjumkvlemres  7463  fodjumkv  7464  nninfwlpoimlemginf  7480  nninfwlpoim  7483  nninfinfwlpo  7484  cardval3ex  7494  prarloclemlo  7825  prarloclem3  7828  cauappcvgprlemdisj  7982  cauappcvgprlemladdru  7987  cauappcvgprlemladdrl  7988  cauappcvgpr  7993  caucvgprlemdisj  8005  caucvgprlemcl  8007  caucvgprlemladdfu  8008  caucvgprlemladdrl  8009  caucvgpr  8013  caucvgprprlemell  8016  caucvgprprlemelu  8017  caucvgprprlemlol  8029  caucvgprprlemclphr  8036  caucvgprprlemexbt  8037  suplocexprlemmu  8049  suplocexpr  8056  suplocsrlem  8139  nntopi  8225  axcaucvglemres  8230  axpre-suploc  8233  suprzclex  9694  supinfneg  9945  infsupneg  9946  ublbneg  9963  suprzubdc  10620  exbtwnzlemstep  10631  exbtwnzlemshrink  10632  rebtwn2zlemstep  10636  rebtwn2zlemshrink  10637  hashunlem  11193  cvg1nlemres  11695  resqrexlemoverl  11731  resqrexlemsqa  11734  resqrexlemex  11735  rexanre  11930  rexico  11931  fimaxre2  11937  summodclem2  12093  summodc  12094  mertenslemub  12245  mertensabs  12248  odd2np1lem  12583  divalglemeunn  12632  divalglemeuneg  12634  bitsfzolem  12665  bezoutlemex  12722  ballotfilemodife  13184  ballotfilemimin  13193  ennnfoneleminc  13246  ennnfonelemex  13249  ennnfonelemhom  13250  ennnfonelemr  13258  ctinfom  13263  nninfdclemp1  13285  nninfdc  13288  cnptoprest  15216  dedekindeulemuub  15594  dedekindeulemub  15595  dedekindeulemloc  15596  dedekindeulemlub  15597  dedekindeulemlu  15598  dedekindicclemuub  15603  dedekindicclemub  15604  dedekindicclemloc  15605  dedekindicclemlub  15606  dedekindicclemlu  15607  ivthdich  15630  bj-nn0sucALT  16860  nconstwlpolem  16963  neapmkvlem  16965