Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  cbvrexv GIF version

Theorem cbvrexv 2534
 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
StepHypRef Expression
1 nfv 1421 . 2 𝑦𝜑
2 nfv 1421 . 2 𝑥𝜓
3 cbvralv.1 . 2 (𝑥 = 𝑦 → (𝜑𝜓))
41, 2, 3cbvrex 2530 1 (∃𝑥𝐴 𝜑 ↔ ∃𝑦𝐴 𝜓)
 Colors of variables: wff set class Syntax hints:   → wi 4   ↔ wb 98  ∃wrex 2307 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022 This theorem depends on definitions:  df-bi 110  df-nf 1350  df-sb 1646  df-cleq 2033  df-clel 2036  df-nfc 2167  df-rex 2312 This theorem is referenced by:  cbvrex2v  2542  reu7  2736  reusv3  4192  funcnvuni  4968  fun11iun  5147  fvelimab  5229  fliftfun  5436  grpridd  5697  frecsuc  5991  nnaordex  6100  cardval3ex  6365  prarloclemlo  6592  prarloclem3  6595  cauappcvgprlemdisj  6749  cauappcvgprlemladdru  6754  cauappcvgprlemladdrl  6755  cauappcvgpr  6760  caucvgprlemdisj  6772  caucvgprlemcl  6774  caucvgprlemladdfu  6775  caucvgprlemladdrl  6776  caucvgpr  6780  caucvgprprlemell  6783  caucvgprprlemelu  6784  caucvgprprlemlol  6796  caucvgprprlemclphr  6803  caucvgprprlemexbt  6804  nntopi  6968  axcaucvglemres  6973  ublbneg  8548  qbtwnzlemstep  9103  qbtwnzlemshrink  9104  rebtwn2zlemstep  9107  rebtwn2zlemshrink  9108  cvg1nlemres  9584  resqrexlemoverl  9619  resqrexlemsqa  9622  resqrexlemex  9623  bj-nn0sucALT  10103
 Copyright terms: Public domain W3C validator