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

Theorem cbval 1637
 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
cbval.2
cbval.3
Assertion
Ref Expression
cbval

Proof of Theorem cbval
StepHypRef Expression
1 cbval.1 . . 3
21nfri 1412 . 2
3 cbval.2 . . 3
43nfri 1412 . 2
5 cbval.3 . 2
62, 4, 5cbvalh 1636 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 98  wal 1241  wnf 1349 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 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427 This theorem depends on definitions:  df-bi 110  df-nf 1350 This theorem is referenced by:  sb8  1736  cbval2  1796  sb8eu  1913  abbi  2151  cleqf  2201  cbvralf  2527  ralab2  2705  cbvralcsf  2908  dfss2f  2936  elintab  3626  cbviota  4872  sb8iota  4874  dffun6f  4915  dffun4f  4918  mptfvex  5256  findcard2  6346  findcard2s  6347
 Copyright terms: Public domain W3C validator