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

Theorem cbvexv 1795
 Description: Rule used to change bound variables, using implicit substitition. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
cbvalv.1
Assertion
Ref Expression
cbvexv
Distinct variable groups:   ,   ,
Allowed substitution hints:   ()   ()

Proof of Theorem cbvexv
StepHypRef Expression
1 ax-17 1419 . 2
2 ax-17 1419 . 2
3 cbvalv.1 . 2
41, 2, 3cbvexh 1638 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 98  wex 1381 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 This theorem is referenced by:  eujust  1902  euind  2728  reuind  2744  r19.3rm  3310  r19.9rmv  3313  raaanlem  3326  raaan  3327  cbvopab2v  3834  bm1.3ii  3878  mss  3962  zfun  4171  xpiindim  4473  relop  4486  dmmrnm  4554  dmxpm  4555  dmcoss  4601  xpm  4745  cnviinm  4859  fv3  5197  fo1stresm  5788  fo2ndresm  5789  iinerm  6178  riinerm  6179  ac6sfi  6352  ltexprlemdisj  6704  ltexprlemloc  6705  recexprlemdisj  6728  climmo  9819  bdbm1.3ii  10011
 Copyright terms: Public domain W3C validator