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  9697  supinfneg  9948  infsupneg  9949  ublbneg  9966  suprzubdc  10623  exbtwnzlemstep  10634  exbtwnzlemshrink  10635  rebtwn2zlemstep  10639  rebtwn2zlemshrink  10640  hashunlem  11196  cvg1nlemres  11699  resqrexlemoverl  11735  resqrexlemsqa  11738  resqrexlemex  11739  rexanre  11934  rexico  11935  fimaxre2  11941  summodclem2  12097  summodc  12098  mertenslemub  12249  mertensabs  12252  odd2np1lem  12587  divalglemeunn  12636  divalglemeuneg  12638  bitsfzolem  12669  bezoutlemex  12726  ballotfilemodife  13188  ballotfilemimin  13197  ennnfoneleminc  13250  ennnfonelemex  13253  ennnfonelemhom  13254  ennnfonelemr  13262  ctinfom  13267  nninfdclemp1  13289  nninfdc  13292  cnptoprest  15234  dedekindeulemuub  15612  dedekindeulemub  15613  dedekindeulemloc  15614  dedekindeulemlub  15615  dedekindeulemlu  15616  dedekindicclemuub  15621  dedekindicclemub  15622  dedekindicclemloc  15623  dedekindicclemlub  15624  dedekindicclemlu  15625  ivthdich  15648  bj-nn0sucALT  16888  nconstwlpolem  16990  neapmkvlem  16992