Theorem cbvrexv 2681

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

Syntax hints:   → wi 4   ↔ wb 104  ∃wrex 2436

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2139

This theorem depends on definitions:  df-bi 116  df-nf 1441  df-sb 1743  df-cleq 2150  df-clel 2153  df-nfc 2288  df-rex 2441

This theorem is referenced by:  cbvrex2v  2692  reu7  2907  reusv3  4418  funcnvuni  5236  fun11iun  5432  fvelimab  5521  fliftfun  5741  grpridd  6011  tfr1onlemaccex  6289  tfrcllemsucaccv  6295  tfrcllembxssdm  6297  tfrcllemaccex  6302  tfrcldm  6304  frecsuc  6348  nnaordex  6467  fimax2gtri  6839  supmoti  6929  suplub2ti  6937  fodjuomnilemdc  7070  fodjuomnilemres  7074  fodjuomni  7075  fodjumkvlemres  7085  fodjumkv  7086  cardval3ex  7103  prarloclemlo  7397  prarloclem3  7400  cauappcvgprlemdisj  7554  cauappcvgprlemladdru  7559  cauappcvgprlemladdrl  7560  cauappcvgpr  7565  caucvgprlemdisj  7577  caucvgprlemcl  7579  caucvgprlemladdfu  7580  caucvgprlemladdrl  7581  caucvgpr  7585  caucvgprprlemell  7588  caucvgprprlemelu  7589  caucvgprprlemlol  7601  caucvgprprlemclphr  7608  caucvgprprlemexbt  7609  suplocexprlemmu  7621  suplocexpr  7628  suplocsrlem  7711  nntopi  7797  axcaucvglemres  7802  axpre-suploc  7805  suprzclex  9245  supinfneg  9489  infsupneg  9490  ublbneg  9504  exbtwnzlemstep  10129  exbtwnzlemshrink  10130  rebtwn2zlemstep  10134  rebtwn2zlemshrink  10135  hashunlem  10660  cvg1nlemres  10867  resqrexlemoverl  10903  resqrexlemsqa  10906  resqrexlemex  10907  rexanre  11102  rexico  11103  fimaxre2  11108  summodclem2  11261  summodc  11262  mertenslemub  11413  mertensabs  11416  odd2np1lem  11744  divalglemeunn  11793  divalglemeuneg  11795  bezoutlemex  11865  ennnfoneleminc  12112  ennnfonelemex  12115  ennnfonelemhom  12116  ennnfonelemr  12124  ctinfom  12129  cnptoprest  12599  dedekindeulemuub  12955  dedekindeulemub  12956  dedekindeulemloc  12957  dedekindeulemlub  12958  dedekindeulemlu  12959  dedekindicclemuub  12964  dedekindicclemub  12965  dedekindicclemloc  12966  dedekindicclemlub  12967  dedekindicclemlu  12968  bj-nn0sucALT  13513  nconstwlpolem  13598  neapmkvlem  13600