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

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

Proof of Theorem cbvex
StepHypRef Expression
1 cbvex.1 . . 3 yφ
21nfri 1393 . 2 (φyφ)
3 cbvex.2 . . 3 xψ
43nfri 1393 . 2 (ψxψ)
5 cbvex.3 . 2 (x = y → (φψ))
62, 4, 5cbvexh 1620 1 (xφyψ)
Colors of variables: wff set class
Syntax hints:  wi 4  wb 98  wnf 1329  wex 1362
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:  sb8e  1719  cbvex2  1779  cbvmo  1922  mo23  1923  clelab  2144  cbvrexf  2506  issetf  2540  eqvincf  2646  rexab2  2684  cbvrexcsf  2886  rabn0m  3222  euabsn  3414  eluniab  3566  cbvopab1  3804  cbvopab2  3805  cbvopab1s  3806  intexabim  3880  iinexgm  3882  opeliunxp  4322  dfdmf  4455  dfrnf  4502  elrnmpt1  4512  cbvoprab1  5499  cbvoprab2  5500  opabex3d  5671  opabex3  5672  bdsepnfALT  7115  strcollnfALT  7204
  Copyright terms: Public domain W3C validator