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

Theorem cbvex 1730
 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 1500 . 2
3 cbvex.2 . . 3
43nfri 1500 . 2
5 cbvex.3 . 2
62, 4, 5cbvexh 1729 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 104  wnf 1437  wex 1469 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515 This theorem depends on definitions:  df-bi 116  df-nf 1438 This theorem is referenced by:  sb8e  1830  cbvex2  1895  cbvmo  2040  mo23  2041  clelab  2266  cbvrexf  2652  issetf  2696  eqvincf  2814  rexab2  2854  cbvrexcsf  3068  abn0m  3393  rabn0m  3395  euabsn  3601  eluniab  3756  cbvopab1  4009  cbvopab2  4010  cbvopab1s  4011  intexabim  4085  iinexgm  4087  opeliunxp  4602  dfdmf  4740  dfrnf  4788  elrnmpt1  4798  cbvoprab1  5851  cbvoprab2  5852  opabex3d  6027  opabex3  6028  seq3f1olemp  10306  fsum2dlemstep  11235  bdsepnfALT  13258  strcollnfALT  13355
 Copyright terms: Public domain W3C validator