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

Theorem cbval 1619
Description: Rule used to change bound variables, using implicit substitution. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 3-Oct-2016.)
Hypotheses
Ref Expression
cbval.1 yφ
cbval.2 xψ
cbval.3 (x = y → (φψ))
Assertion
Ref Expression
cbval (xφyψ)

Proof of Theorem cbval
StepHypRef Expression
1 cbval.1 . . 3 yφ
21nfri 1393 . 2 (φyφ)
3 cbval.2 . . 3 xψ
43nfri 1393 . 2 (ψxψ)
5 cbval.3 . 2 (x = y → (φψ))
62, 4, 5cbvalh 1618 1 (xφyψ)
Colors of variables: wff set class
Syntax hints:  wi 4  wb 98  wal 1226  wnf 1329
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-5 1316  ax-7 1317  ax-gen 1318  ax-ie1 1363  ax-ie2 1364  ax-8 1376  ax-4 1381  ax-17 1400  ax-i9 1404  ax-ial 1409
This theorem depends on definitions:  df-bi 110  df-nf 1330
This theorem is referenced by:  sb8  1718  cbval2  1778  sb8eu  1895  abbi  2133  cleqf  2183  cbvralf  2505  ralab2  2682  cbvralcsf  2885  dfss2f  2913  elintab  3600  cbviota  4799  sb8iota  4801  dffun6f  4841  dffun4f  4844  mptfvex  5181
  Copyright terms: Public domain W3C validator