ILE Home 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  6363  prarloclemlo  6590  prarloclem3  6593  cauappcvgprlemdisj  6747  cauappcvgprlemladdru  6752  cauappcvgprlemladdrl  6753  cauappcvgpr  6758  caucvgprlemdisj  6770  caucvgprlemcl  6772  caucvgprlemladdfu  6773  caucvgprlemladdrl  6774  caucvgpr  6778  caucvgprprlemell  6781  caucvgprprlemelu  6782  caucvgprprlemlol  6794  caucvgprprlemclphr  6801  caucvgprprlemexbt  6802  nntopi  6966  axcaucvglemres  6971  ublbneg  8546  qbtwnzlemstep  9101  qbtwnzlemshrink  9102  rebtwn2zlemstep  9105  rebtwn2zlemshrink  9106  cvg1nlemres  9558  resqrexlemoverl  9593  resqrexlemsqa  9596  resqrexlemex  9597  bj-nn0sucALT  10077
  Copyright terms: Public domain W3C validator