Theorem cbvrexv 2787

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

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

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 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-cleq 2231  df-clel 2234  df-nfc 2381  df-rex 2534

This theorem is referenced by:  cbvrex2v  2800  reu7  3021  reusv3  4604  funcnvuni  5448  fun11iun  5658  fvelimab  5756  fliftfun  5996  tfr1onlemaccex  6613  tfrcllemsucaccv  6619  tfrcllembxssdm  6621  tfrcllemaccex  6626  tfrcldm  6628  frecsuc  6672  nnaordex  6795  fimax2gtri  7200  supmoti  7327  suplub2ti  7335  fodjuomnilemdc  7478  fodjuomnilemres  7482  fodjuomni  7483  fodjumkvlemres  7493  fodjumkv  7494  nninfwlpoimlemginf  7510  nninfwlpoim  7513  nninfinfwlpo  7514  cardval3ex  7524  prarloclemlo  7855  prarloclem3  7858  cauappcvgprlemdisj  8012  cauappcvgprlemladdru  8017  cauappcvgprlemladdrl  8018  cauappcvgpr  8023  caucvgprlemdisj  8035  caucvgprlemcl  8037  caucvgprlemladdfu  8038  caucvgprlemladdrl  8039  caucvgpr  8043  caucvgprprlemell  8046  caucvgprprlemelu  8047  caucvgprprlemlol  8059  caucvgprprlemclphr  8066  caucvgprprlemexbt  8067  suplocexprlemmu  8079  suplocexpr  8086  suplocsrlem  8169  nntopi  8255  axcaucvglemres  8260  axpre-suploc  8263  suprzclex  9727  supinfneg  9978  infsupneg  9979  ublbneg  9996  suprzubdc  10654  exbtwnzlemstep  10665  exbtwnzlemshrink  10666  rebtwn2zlemstep  10670  rebtwn2zlemshrink  10671  hashunlem  11227  cvg1nlemres  11734  resqrexlemoverl  11770  resqrexlemsqa  11773  resqrexlemex  11774  rexanre  11969  rexico  11970  fimaxre2  11976  summodclem2  12132  summodc  12133  mertenslemub  12284  mertensabs  12287  odd2np1lem  12622  divalglemeunn  12671  divalglemeuneg  12673  bitsfzolem  12704  bezoutlemex  12761  ballotfilemodife  13223  ballotfilemimin  13232  ennnfoneleminc  13285  ennnfonelemex  13288  ennnfonelemhom  13289  ennnfonelemr  13297  ctinfom  13302  nninfdclemp1  13324  nninfdc  13327  cnptoprest  15323  dedekindeulemuub  15701  dedekindeulemub  15702  dedekindeulemloc  15703  dedekindeulemlub  15704  dedekindeulemlu  15705  dedekindicclemuub  15710  dedekindicclemub  15711  dedekindicclemloc  15712  dedekindicclemlub  15713  dedekindicclemlu  15714  ivthdich  15737  bj-nn0sucALT  16987  nconstwlpolem  17089  neapmkvlem  17091