Theorem cbvrexv 2716

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

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

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 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-10 1515  ax-11 1516  ax-i12 1517  ax-bndl 1519  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-ext 2169

This theorem depends on definitions:  df-bi 117  df-nf 1471  df-sb 1773  df-cleq 2180  df-clel 2183  df-nfc 2318  df-rex 2471

This theorem is referenced by:  cbvrex2v  2729  reu7  2944  reusv3  4472  funcnvuni  5297  fun11iun  5494  fvelimab  5585  fliftfun  5810  tfr1onlemaccex  6363  tfrcllemsucaccv  6369  tfrcllembxssdm  6371  tfrcllemaccex  6376  tfrcldm  6378  frecsuc  6422  nnaordex  6543  fimax2gtri  6915  supmoti  7006  suplub2ti  7014  fodjuomnilemdc  7156  fodjuomnilemres  7160  fodjuomni  7161  fodjumkvlemres  7171  fodjumkv  7172  nninfwlpoimlemginf  7188  nninfwlpoim  7190  cardval3ex  7198  prarloclemlo  7507  prarloclem3  7510  cauappcvgprlemdisj  7664  cauappcvgprlemladdru  7669  cauappcvgprlemladdrl  7670  cauappcvgpr  7675  caucvgprlemdisj  7687  caucvgprlemcl  7689  caucvgprlemladdfu  7690  caucvgprlemladdrl  7691  caucvgpr  7695  caucvgprprlemell  7698  caucvgprprlemelu  7699  caucvgprprlemlol  7711  caucvgprprlemclphr  7718  caucvgprprlemexbt  7719  suplocexprlemmu  7731  suplocexpr  7738  suplocsrlem  7821  nntopi  7907  axcaucvglemres  7912  axpre-suploc  7915  suprzclex  9365  supinfneg  9609  infsupneg  9610  ublbneg  9627  exbtwnzlemstep  10262  exbtwnzlemshrink  10263  rebtwn2zlemstep  10267  rebtwn2zlemshrink  10268  hashunlem  10798  cvg1nlemres  11008  resqrexlemoverl  11044  resqrexlemsqa  11047  resqrexlemex  11048  rexanre  11243  rexico  11244  fimaxre2  11249  summodclem2  11404  summodc  11405  mertenslemub  11556  mertensabs  11559  odd2np1lem  11891  divalglemeunn  11940  divalglemeuneg  11942  suprzubdc  11967  bezoutlemex  12016  ennnfoneleminc  12426  ennnfonelemex  12429  ennnfonelemhom  12430  ennnfonelemr  12438  ctinfom  12443  nninfdclemcl  12463  nninfdclemp1  12465  nninfdc  12468  cnptoprest  14035  dedekindeulemuub  14391  dedekindeulemub  14392  dedekindeulemloc  14393  dedekindeulemlub  14394  dedekindeulemlu  14395  dedekindicclemuub  14400  dedekindicclemub  14401  dedekindicclemloc  14402  dedekindicclemlub  14403  dedekindicclemlu  14404  bj-nn0sucALT  15026  nconstwlpolem  15110  neapmkvlem  15112