Theorem cbvrexv 2766

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

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

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-cleq 2222  df-clel 2225  df-nfc 2361  df-rex 2514

This theorem is referenced by:  cbvrex2v  2779  reu7  2998  reusv3  4552  funcnvuni  5393  fun11iun  5598  fvelimab  5695  fliftfun  5929  tfr1onlemaccex  6505  tfrcllemsucaccv  6511  tfrcllembxssdm  6513  tfrcllemaccex  6518  tfrcldm  6520  frecsuc  6564  nnaordex  6687  fimax2gtri  7077  supmoti  7176  suplub2ti  7184  fodjuomnilemdc  7327  fodjuomnilemres  7331  fodjuomni  7332  fodjumkvlemres  7342  fodjumkv  7343  nninfwlpoimlemginf  7359  nninfwlpoim  7362  nninfinfwlpo  7363  cardval3ex  7373  prarloclemlo  7697  prarloclem3  7700  cauappcvgprlemdisj  7854  cauappcvgprlemladdru  7859  cauappcvgprlemladdrl  7860  cauappcvgpr  7865  caucvgprlemdisj  7877  caucvgprlemcl  7879  caucvgprlemladdfu  7880  caucvgprlemladdrl  7881  caucvgpr  7885  caucvgprprlemell  7888  caucvgprprlemelu  7889  caucvgprprlemlol  7901  caucvgprprlemclphr  7908  caucvgprprlemexbt  7909  suplocexprlemmu  7921  suplocexpr  7928  suplocsrlem  8011  nntopi  8097  axcaucvglemres  8102  axpre-suploc  8105  suprzclex  9561  supinfneg  9807  infsupneg  9808  ublbneg  9825  suprzubdc  10473  exbtwnzlemstep  10484  exbtwnzlemshrink  10485  rebtwn2zlemstep  10489  rebtwn2zlemshrink  10490  hashunlem  11043  cvg1nlemres  11517  resqrexlemoverl  11553  resqrexlemsqa  11556  resqrexlemex  11557  rexanre  11752  rexico  11753  fimaxre2  11759  summodclem2  11914  summodc  11915  mertenslemub  12066  mertensabs  12069  odd2np1lem  12404  divalglemeunn  12453  divalglemeuneg  12455  bitsfzolem  12486  bezoutlemex  12543  ennnfoneleminc  13003  ennnfonelemex  13006  ennnfonelemhom  13007  ennnfonelemr  13015  ctinfom  13020  nninfdclemp1  13042  nninfdc  13045  cnptoprest  14934  dedekindeulemuub  15312  dedekindeulemub  15313  dedekindeulemloc  15314  dedekindeulemlub  15315  dedekindeulemlu  15316  dedekindicclemuub  15321  dedekindicclemub  15322  dedekindicclemloc  15323  dedekindicclemlub  15324  dedekindicclemlu  15325  ivthdich  15348  bj-nn0sucALT  16450  nconstwlpolem  16547  neapmkvlem  16549