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

Theorem cbvrexv 2531
Description: Change the bound variable of a restricted existential quantifier using implicit substitution. (Contributed by NM, 2-Jun-1998.)
Hypothesis
Ref Expression
cbvralv.1 (x = y → (φψ))
Assertion
Ref Expression
cbvrexv (x A φy A ψ)
Distinct variable groups:   x,A   y,A   φ,y   ψ,x
Allowed substitution hints:   φ(x)   ψ(y)

Proof of Theorem cbvrexv
StepHypRef Expression
1 nfv 1421 . 2 yφ
2 nfv 1421 . 2 xψ
3 cbvralv.1 . 2 (x = y → (φψ))
41, 2, 3cbvrex 2527 1 (x A φy A ψ)
Colors of variables: wff set class
Syntax hints:  wi 4  wb 98  wrex 2304
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 2309
This theorem is referenced by:  cbvrex2v  2539  reu7  2733  reusv3  4161  funcnvuni  4914  fun11iun  5093  fvelimab  5175  fliftfun  5382  grpridd  5642  frecsuc  5934  nnaordex  6040  prarloclemlo  6482  prarloclem3  6485  cauappcvgprlemdisj  6639  cauappcvgprlemladdru  6644  cauappcvgprlemladdrl  6645  cauappcvgpr  6650  caucvgprlemdisj  6662  caucvgprlemcl  6664  caucvgprlemladdfu  6665  caucvgprlemladdrl  6666  caucvgpr  6670  caucvgprprlemell  6673  caucvgprprlemelu  6674  caucvgprprlemlol  6686  caucvgprprlemclphr  6693  caucvgprprlemexbt  6694  nntopi  6858  axcaucvglemres  6863  ublbneg  8416  bj-nn0sucALT  9546
  Copyright terms: Public domain W3C validator