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  4551  funcnvuni  5390  fun11iun  5595  fvelimab  5692  fliftfun  5926  tfr1onlemaccex  6500  tfrcllemsucaccv  6506  tfrcllembxssdm  6508  tfrcllemaccex  6513  tfrcldm  6515  frecsuc  6559  nnaordex  6682  fimax2gtri  7071  supmoti  7168  suplub2ti  7176  fodjuomnilemdc  7319  fodjuomnilemres  7323  fodjuomni  7324  fodjumkvlemres  7334  fodjumkv  7335  nninfwlpoimlemginf  7351  nninfwlpoim  7354  nninfinfwlpo  7355  cardval3ex  7365  prarloclemlo  7689  prarloclem3  7692  cauappcvgprlemdisj  7846  cauappcvgprlemladdru  7851  cauappcvgprlemladdrl  7852  cauappcvgpr  7857  caucvgprlemdisj  7869  caucvgprlemcl  7871  caucvgprlemladdfu  7872  caucvgprlemladdrl  7873  caucvgpr  7877  caucvgprprlemell  7880  caucvgprprlemelu  7881  caucvgprprlemlol  7893  caucvgprprlemclphr  7900  caucvgprprlemexbt  7901  suplocexprlemmu  7913  suplocexpr  7920  suplocsrlem  8003  nntopi  8089  axcaucvglemres  8094  axpre-suploc  8097  suprzclex  9553  supinfneg  9798  infsupneg  9799  ublbneg  9816  suprzubdc  10464  exbtwnzlemstep  10475  exbtwnzlemshrink  10476  rebtwn2zlemstep  10480  rebtwn2zlemshrink  10481  hashunlem  11034  cvg1nlemres  11504  resqrexlemoverl  11540  resqrexlemsqa  11543  resqrexlemex  11544  rexanre  11739  rexico  11740  fimaxre2  11746  summodclem2  11901  summodc  11902  mertenslemub  12053  mertensabs  12056  odd2np1lem  12391  divalglemeunn  12440  divalglemeuneg  12442  bitsfzolem  12473  bezoutlemex  12530  ennnfoneleminc  12990  ennnfonelemex  12993  ennnfonelemhom  12994  ennnfonelemr  13002  ctinfom  13007  nninfdclemp1  13029  nninfdc  13032  cnptoprest  14921  dedekindeulemuub  15299  dedekindeulemub  15300  dedekindeulemloc  15301  dedekindeulemlub  15302  dedekindeulemlu  15303  dedekindicclemuub  15308  dedekindicclemub  15309  dedekindicclemloc  15310  dedekindicclemlub  15311  dedekindicclemlu  15312  ivthdich  15335  bj-nn0sucALT  16365  nconstwlpolem  16463  neapmkvlem  16465