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

Theorem cbvex 1636
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 1409 . 2 (φyφ)
3 cbvex.2 . . 3 xψ
43nfri 1409 . 2 (ψxψ)
5 cbvex.3 . 2 (x = y → (φψ))
62, 4, 5cbvexh 1635 1 (xφyψ)
Colors of variables: wff set class
Syntax hints:  wi 4  wb 98  wnf 1346  wex 1378
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 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-4 1397  ax-17 1416  ax-i9 1420  ax-ial 1424
This theorem depends on definitions:  df-bi 110  df-nf 1347
This theorem is referenced by:  sb8e  1734  cbvex2  1794  cbvmo  1937  mo23  1938  clelab  2159  cbvrexf  2522  issetf  2556  eqvincf  2663  rexab2  2701  cbvrexcsf  2903  rabn0m  3239  euabsn  3431  eluniab  3583  cbvopab1  3821  cbvopab2  3822  cbvopab1s  3823  intexabim  3897  iinexgm  3899  opeliunxp  4338  dfdmf  4471  dfrnf  4518  elrnmpt1  4528  cbvoprab1  5518  cbvoprab2  5519  opabex3d  5690  opabex3  5691  bdsepnfALT  9277  strcollnfALT  9370
  Copyright terms: Public domain W3C validator