Theorem cbvrexv 2705

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 2701	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  2718  reu7  2933  reusv3  4461  funcnvuni  5286  fun11iun  5483  fvelimab  5573  fliftfun  5797  tfr1onlemaccex  6349  tfrcllemsucaccv  6355  tfrcllembxssdm  6357  tfrcllemaccex  6362  tfrcldm  6364  frecsuc  6408  nnaordex  6529  fimax2gtri  6901  supmoti  6992  suplub2ti  7000  fodjuomnilemdc  7142  fodjuomnilemres  7146  fodjuomni  7147  fodjumkvlemres  7157  fodjumkv  7158  nninfwlpoimlemginf  7174  nninfwlpoim  7176  cardval3ex  7184  prarloclemlo  7493  prarloclem3  7496  cauappcvgprlemdisj  7650  cauappcvgprlemladdru  7655  cauappcvgprlemladdrl  7656  cauappcvgpr  7661  caucvgprlemdisj  7673  caucvgprlemcl  7675  caucvgprlemladdfu  7676  caucvgprlemladdrl  7677  caucvgpr  7681  caucvgprprlemell  7684  caucvgprprlemelu  7685  caucvgprprlemlol  7697  caucvgprprlemclphr  7704  caucvgprprlemexbt  7705  suplocexprlemmu  7717  suplocexpr  7724  suplocsrlem  7807  nntopi  7893  axcaucvglemres  7898  axpre-suploc  7901  suprzclex  9351  supinfneg  9595  infsupneg  9596  ublbneg  9613  exbtwnzlemstep  10248  exbtwnzlemshrink  10249  rebtwn2zlemstep  10253  rebtwn2zlemshrink  10254  hashunlem  10784  cvg1nlemres  10994  resqrexlemoverl  11030  resqrexlemsqa  11033  resqrexlemex  11034  rexanre  11229  rexico  11230  fimaxre2  11235  summodclem2  11390  summodc  11391  mertenslemub  11542  mertensabs  11545  odd2np1lem  11877  divalglemeunn  11926  divalglemeuneg  11928  suprzubdc  11953  bezoutlemex  12002  ennnfoneleminc  12412  ennnfonelemex  12415  ennnfonelemhom  12416  ennnfonelemr  12424  ctinfom  12429  nninfdclemcl  12449  nninfdclemp1  12451  nninfdc  12454  cnptoprest  13742  dedekindeulemuub  14098  dedekindeulemub  14099  dedekindeulemloc  14100  dedekindeulemlub  14101  dedekindeulemlu  14102  dedekindicclemuub  14107  dedekindicclemub  14108  dedekindicclemloc  14109  dedekindicclemlub  14110  dedekindicclemlu  14111  bj-nn0sucALT  14733  nconstwlpolem  14815  neapmkvlem  14817