Theorem cbvrexv 2769

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

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

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 2213

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1811  df-cleq 2224  df-clel 2227  df-nfc 2364  df-rex 2517

This theorem is referenced by:  cbvrex2v  2782  reu7  3002  reusv3  4563  funcnvuni  5406  fun11iun  5613  fvelimab  5711  fliftfun  5947  tfr1onlemaccex  6557  tfrcllemsucaccv  6563  tfrcllembxssdm  6565  tfrcllemaccex  6570  tfrcldm  6572  frecsuc  6616  nnaordex  6739  fimax2gtri  7134  supmoti  7235  suplub2ti  7243  fodjuomnilemdc  7386  fodjuomnilemres  7390  fodjuomni  7391  fodjumkvlemres  7401  fodjumkv  7402  nninfwlpoimlemginf  7418  nninfwlpoim  7421  nninfinfwlpo  7422  cardval3ex  7432  prarloclemlo  7757  prarloclem3  7760  cauappcvgprlemdisj  7914  cauappcvgprlemladdru  7919  cauappcvgprlemladdrl  7920  cauappcvgpr  7925  caucvgprlemdisj  7937  caucvgprlemcl  7939  caucvgprlemladdfu  7940  caucvgprlemladdrl  7941  caucvgpr  7945  caucvgprprlemell  7948  caucvgprprlemelu  7949  caucvgprprlemlol  7961  caucvgprprlemclphr  7968  caucvgprprlemexbt  7969  suplocexprlemmu  7981  suplocexpr  7988  suplocsrlem  8071  nntopi  8157  axcaucvglemres  8162  axpre-suploc  8165  suprzclex  9621  supinfneg  9872  infsupneg  9873  ublbneg  9890  suprzubdc  10540  exbtwnzlemstep  10551  exbtwnzlemshrink  10552  rebtwn2zlemstep  10556  rebtwn2zlemshrink  10557  hashunlem  11111  cvg1nlemres  11606  resqrexlemoverl  11642  resqrexlemsqa  11645  resqrexlemex  11646  rexanre  11841  rexico  11842  fimaxre2  11848  summodclem2  12004  summodc  12005  mertenslemub  12156  mertensabs  12159  odd2np1lem  12494  divalglemeunn  12543  divalglemeuneg  12545  bitsfzolem  12576  bezoutlemex  12633  ennnfoneleminc  13093  ennnfonelemex  13096  ennnfonelemhom  13097  ennnfonelemr  13105  ctinfom  13110  nninfdclemp1  13132  nninfdc  13135  cnptoprest  15030  dedekindeulemuub  15408  dedekindeulemub  15409  dedekindeulemloc  15410  dedekindeulemlub  15411  dedekindeulemlu  15412  dedekindicclemuub  15417  dedekindicclemub  15418  dedekindicclemloc  15419  dedekindicclemlub  15420  dedekindicclemlu  15421  ivthdich  15444  bj-nn0sucALT  16674  nconstwlpolem  16778  neapmkvlem  16780