Theorem cbvrexv 2730

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

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

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 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-sb 1777  df-cleq 2189  df-clel 2192  df-nfc 2328  df-rex 2481

This theorem is referenced by:  cbvrex2v  2743  reu7  2959  reusv3  4495  funcnvuni  5327  fun11iun  5525  fvelimab  5617  fliftfun  5843  tfr1onlemaccex  6406  tfrcllemsucaccv  6412  tfrcllembxssdm  6414  tfrcllemaccex  6419  tfrcldm  6421  frecsuc  6465  nnaordex  6586  fimax2gtri  6962  supmoti  7059  suplub2ti  7067  fodjuomnilemdc  7210  fodjuomnilemres  7214  fodjuomni  7215  fodjumkvlemres  7225  fodjumkv  7226  nninfwlpoimlemginf  7242  nninfwlpoim  7244  cardval3ex  7252  prarloclemlo  7561  prarloclem3  7564  cauappcvgprlemdisj  7718  cauappcvgprlemladdru  7723  cauappcvgprlemladdrl  7724  cauappcvgpr  7729  caucvgprlemdisj  7741  caucvgprlemcl  7743  caucvgprlemladdfu  7744  caucvgprlemladdrl  7745  caucvgpr  7749  caucvgprprlemell  7752  caucvgprprlemelu  7753  caucvgprprlemlol  7765  caucvgprprlemclphr  7772  caucvgprprlemexbt  7773  suplocexprlemmu  7785  suplocexpr  7792  suplocsrlem  7875  nntopi  7961  axcaucvglemres  7966  axpre-suploc  7969  suprzclex  9424  supinfneg  9669  infsupneg  9670  ublbneg  9687  suprzubdc  10326  exbtwnzlemstep  10337  exbtwnzlemshrink  10338  rebtwn2zlemstep  10342  rebtwn2zlemshrink  10343  hashunlem  10896  cvg1nlemres  11150  resqrexlemoverl  11186  resqrexlemsqa  11189  resqrexlemex  11190  rexanre  11385  rexico  11386  fimaxre2  11392  summodclem2  11547  summodc  11548  mertenslemub  11699  mertensabs  11702  odd2np1lem  12037  divalglemeunn  12086  divalglemeuneg  12088  bitsfzolem  12118  bezoutlemex  12168  ennnfoneleminc  12628  ennnfonelemex  12631  ennnfonelemhom  12632  ennnfonelemr  12640  ctinfom  12645  nninfdclemp1  12667  nninfdc  12670  cnptoprest  14475  dedekindeulemuub  14853  dedekindeulemub  14854  dedekindeulemloc  14855  dedekindeulemlub  14856  dedekindeulemlu  14857  dedekindicclemuub  14862  dedekindicclemub  14863  dedekindicclemloc  14864  dedekindicclemlub  14865  dedekindicclemlu  14866  ivthdich  14889  bj-nn0sucALT  15624  nconstwlpolem  15709  neapmkvlem  15711