Theorem cbvrexv 2740

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

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

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-sb 1787  df-cleq 2199  df-clel 2202  df-nfc 2338  df-rex 2491

This theorem is referenced by:  cbvrex2v  2753  reu7  2970  reusv3  4512  funcnvuni  5349  fun11iun  5552  fvelimab  5645  fliftfun  5875  tfr1onlemaccex  6444  tfrcllemsucaccv  6450  tfrcllembxssdm  6452  tfrcllemaccex  6457  tfrcldm  6459  frecsuc  6503  nnaordex  6624  fimax2gtri  7010  supmoti  7107  suplub2ti  7115  fodjuomnilemdc  7258  fodjuomnilemres  7262  fodjuomni  7263  fodjumkvlemres  7273  fodjumkv  7274  nninfwlpoimlemginf  7290  nninfwlpoim  7293  nninfinfwlpo  7294  cardval3ex  7304  prarloclemlo  7620  prarloclem3  7623  cauappcvgprlemdisj  7777  cauappcvgprlemladdru  7782  cauappcvgprlemladdrl  7783  cauappcvgpr  7788  caucvgprlemdisj  7800  caucvgprlemcl  7802  caucvgprlemladdfu  7803  caucvgprlemladdrl  7804  caucvgpr  7808  caucvgprprlemell  7811  caucvgprprlemelu  7812  caucvgprprlemlol  7824  caucvgprprlemclphr  7831  caucvgprprlemexbt  7832  suplocexprlemmu  7844  suplocexpr  7851  suplocsrlem  7934  nntopi  8020  axcaucvglemres  8025  axpre-suploc  8028  suprzclex  9484  supinfneg  9729  infsupneg  9730  ublbneg  9747  suprzubdc  10392  exbtwnzlemstep  10403  exbtwnzlemshrink  10404  rebtwn2zlemstep  10408  rebtwn2zlemshrink  10409  hashunlem  10962  cvg1nlemres  11346  resqrexlemoverl  11382  resqrexlemsqa  11385  resqrexlemex  11386  rexanre  11581  rexico  11582  fimaxre2  11588  summodclem2  11743  summodc  11744  mertenslemub  11895  mertensabs  11898  odd2np1lem  12233  divalglemeunn  12282  divalglemeuneg  12284  bitsfzolem  12315  bezoutlemex  12372  ennnfoneleminc  12832  ennnfonelemex  12835  ennnfonelemhom  12836  ennnfonelemr  12844  ctinfom  12849  nninfdclemp1  12871  nninfdc  12874  cnptoprest  14761  dedekindeulemuub  15139  dedekindeulemub  15140  dedekindeulemloc  15141  dedekindeulemlub  15142  dedekindeulemlu  15143  dedekindicclemuub  15148  dedekindicclemub  15149  dedekindicclemloc  15150  dedekindicclemlub  15151  dedekindicclemlu  15152  ivthdich  15175  bj-nn0sucALT  16028  nconstwlpolem  16119  neapmkvlem  16121