Theorem cbvrexv 2768

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

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

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1811  df-cleq 2224  df-clel 2227  df-nfc 2363  df-rex 2516

This theorem is referenced by:  cbvrex2v  2781  reu7  3001  reusv3  4557  funcnvuni  5399  fun11iun  5604  fvelimab  5702  fliftfun  5937  tfr1onlemaccex  6514  tfrcllemsucaccv  6520  tfrcllembxssdm  6522  tfrcllemaccex  6527  tfrcldm  6529  frecsuc  6573  nnaordex  6696  fimax2gtri  7091  supmoti  7192  suplub2ti  7200  fodjuomnilemdc  7343  fodjuomnilemres  7347  fodjuomni  7348  fodjumkvlemres  7358  fodjumkv  7359  nninfwlpoimlemginf  7375  nninfwlpoim  7378  nninfinfwlpo  7379  cardval3ex  7389  prarloclemlo  7714  prarloclem3  7717  cauappcvgprlemdisj  7871  cauappcvgprlemladdru  7876  cauappcvgprlemladdrl  7877  cauappcvgpr  7882  caucvgprlemdisj  7894  caucvgprlemcl  7896  caucvgprlemladdfu  7897  caucvgprlemladdrl  7898  caucvgpr  7902  caucvgprprlemell  7905  caucvgprprlemelu  7906  caucvgprprlemlol  7918  caucvgprprlemclphr  7925  caucvgprprlemexbt  7926  suplocexprlemmu  7938  suplocexpr  7945  suplocsrlem  8028  nntopi  8114  axcaucvglemres  8119  axpre-suploc  8122  suprzclex  9578  supinfneg  9829  infsupneg  9830  ublbneg  9847  suprzubdc  10496  exbtwnzlemstep  10507  exbtwnzlemshrink  10508  rebtwn2zlemstep  10512  rebtwn2zlemshrink  10513  hashunlem  11067  cvg1nlemres  11546  resqrexlemoverl  11582  resqrexlemsqa  11585  resqrexlemex  11586  rexanre  11781  rexico  11782  fimaxre2  11788  summodclem2  11944  summodc  11945  mertenslemub  12096  mertensabs  12099  odd2np1lem  12434  divalglemeunn  12483  divalglemeuneg  12485  bitsfzolem  12516  bezoutlemex  12573  ennnfoneleminc  13033  ennnfonelemex  13036  ennnfonelemhom  13037  ennnfonelemr  13045  ctinfom  13050  nninfdclemp1  13072  nninfdc  13075  cnptoprest  14965  dedekindeulemuub  15343  dedekindeulemub  15344  dedekindeulemloc  15345  dedekindeulemlub  15346  dedekindeulemlu  15347  dedekindicclemuub  15352  dedekindicclemub  15353  dedekindicclemloc  15354  dedekindicclemlub  15355  dedekindicclemlu  15356  ivthdich  15379  bj-nn0sucALT  16576  nconstwlpolem  16672  neapmkvlem  16674