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  2999  reusv3  4555  funcnvuni  5396  fun11iun  5601  fvelimab  5698  fliftfun  5932  tfr1onlemaccex  6509  tfrcllemsucaccv  6515  tfrcllembxssdm  6517  tfrcllemaccex  6522  tfrcldm  6524  frecsuc  6568  nnaordex  6691  fimax2gtri  7086  supmoti  7186  suplub2ti  7194  fodjuomnilemdc  7337  fodjuomnilemres  7341  fodjuomni  7342  fodjumkvlemres  7352  fodjumkv  7353  nninfwlpoimlemginf  7369  nninfwlpoim  7372  nninfinfwlpo  7373  cardval3ex  7383  prarloclemlo  7707  prarloclem3  7710  cauappcvgprlemdisj  7864  cauappcvgprlemladdru  7869  cauappcvgprlemladdrl  7870  cauappcvgpr  7875  caucvgprlemdisj  7887  caucvgprlemcl  7889  caucvgprlemladdfu  7890  caucvgprlemladdrl  7891  caucvgpr  7895  caucvgprprlemell  7898  caucvgprprlemelu  7899  caucvgprprlemlol  7911  caucvgprprlemclphr  7918  caucvgprprlemexbt  7919  suplocexprlemmu  7931  suplocexpr  7938  suplocsrlem  8021  nntopi  8107  axcaucvglemres  8112  axpre-suploc  8115  suprzclex  9571  supinfneg  9822  infsupneg  9823  ublbneg  9840  suprzubdc  10489  exbtwnzlemstep  10500  exbtwnzlemshrink  10501  rebtwn2zlemstep  10505  rebtwn2zlemshrink  10506  hashunlem  11060  cvg1nlemres  11539  resqrexlemoverl  11575  resqrexlemsqa  11578  resqrexlemex  11579  rexanre  11774  rexico  11775  fimaxre2  11781  summodclem2  11936  summodc  11937  mertenslemub  12088  mertensabs  12091  odd2np1lem  12426  divalglemeunn  12475  divalglemeuneg  12477  bitsfzolem  12508  bezoutlemex  12565  ennnfoneleminc  13025  ennnfonelemex  13028  ennnfonelemhom  13029  ennnfonelemr  13037  ctinfom  13042  nninfdclemp1  13064  nninfdc  13067  cnptoprest  14956  dedekindeulemuub  15334  dedekindeulemub  15335  dedekindeulemloc  15336  dedekindeulemlub  15337  dedekindeulemlu  15338  dedekindicclemuub  15343  dedekindicclemub  15344  dedekindicclemloc  15345  dedekindicclemlub  15346  dedekindicclemlu  15347  ivthdich  15370  bj-nn0sucALT  16523  nconstwlpolem  16619  neapmkvlem  16621