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

Theorem cbvex 1639
 Description: Rule used to change bound variables, using implicit substitution. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
cbvex.1
cbvex.2
cbvex.3
Assertion
Ref Expression
cbvex

Proof of Theorem cbvex
StepHypRef Expression
1 cbvex.1 . . 3
21nfri 1412 . 2
3 cbvex.2 . . 3
43nfri 1412 . 2
5 cbvex.3 . 2
62, 4, 5cbvexh 1638 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 98  wnf 1349  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  df-nf 1350 This theorem is referenced by:  sb8e  1737  cbvex2  1797  cbvmo  1940  mo23  1941  clelab  2162  cbvrexf  2528  issetf  2562  eqvincf  2669  rexab2  2707  cbvrexcsf  2909  rabn0m  3245  euabsn  3440  eluniab  3592  cbvopab1  3830  cbvopab2  3831  cbvopab1s  3832  intexabim  3906  iinexgm  3908  opeliunxp  4395  dfdmf  4528  dfrnf  4575  elrnmpt1  4585  cbvoprab1  5576  cbvoprab2  5577  opabex3d  5748  opabex3  5749  bdsepnfALT  10009  strcollnfALT  10111
 Copyright terms: Public domain W3C validator