Theorem cbvrexv 2704

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

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

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-cleq 2170  df-clel 2173  df-nfc 2308  df-rex 2461

This theorem is referenced by:  cbvrex2v  2717  reu7  2932  reusv3  4460  funcnvuni  5285  fun11iun  5482  fvelimab  5572  fliftfun  5796  tfr1onlemaccex  6348  tfrcllemsucaccv  6354  tfrcllembxssdm  6356  tfrcllemaccex  6361  tfrcldm  6363  frecsuc  6407  nnaordex  6528  fimax2gtri  6900  supmoti  6991  suplub2ti  6999  fodjuomnilemdc  7141  fodjuomnilemres  7145  fodjuomni  7146  fodjumkvlemres  7156  fodjumkv  7157  nninfwlpoimlemginf  7173  nninfwlpoim  7175  cardval3ex  7183  prarloclemlo  7492  prarloclem3  7495  cauappcvgprlemdisj  7649  cauappcvgprlemladdru  7654  cauappcvgprlemladdrl  7655  cauappcvgpr  7660  caucvgprlemdisj  7672  caucvgprlemcl  7674  caucvgprlemladdfu  7675  caucvgprlemladdrl  7676  caucvgpr  7680  caucvgprprlemell  7683  caucvgprprlemelu  7684  caucvgprprlemlol  7696  caucvgprprlemclphr  7703  caucvgprprlemexbt  7704  suplocexprlemmu  7716  suplocexpr  7723  suplocsrlem  7806  nntopi  7892  axcaucvglemres  7897  axpre-suploc  7900  suprzclex  9350  supinfneg  9594  infsupneg  9595  ublbneg  9612  exbtwnzlemstep  10247  exbtwnzlemshrink  10248  rebtwn2zlemstep  10252  rebtwn2zlemshrink  10253  hashunlem  10783  cvg1nlemres  10993  resqrexlemoverl  11029  resqrexlemsqa  11032  resqrexlemex  11033  rexanre  11228  rexico  11229  fimaxre2  11234  summodclem2  11389  summodc  11390  mertenslemub  11541  mertensabs  11544  odd2np1lem  11876  divalglemeunn  11925  divalglemeuneg  11927  suprzubdc  11952  bezoutlemex  12001  ennnfoneleminc  12411  ennnfonelemex  12414  ennnfonelemhom  12415  ennnfonelemr  12423  ctinfom  12428  nninfdclemcl  12448  nninfdclemp1  12450  nninfdc  12453  cnptoprest  13709  dedekindeulemuub  14065  dedekindeulemub  14066  dedekindeulemloc  14067  dedekindeulemlub  14068  dedekindeulemlu  14069  dedekindicclemuub  14074  dedekindicclemub  14075  dedekindicclemloc  14076  dedekindicclemlub  14077  dedekindicclemlu  14078  bj-nn0sucALT  14700  nconstwlpolem  14782  neapmkvlem  14784