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

Theorem sbie 1656
 Description: Conversion of implicit substitution to explicit substitution. (Contributed by NM, 30-Jun-1994.) (Revised by Mario Carneiro, 4-Oct-2016.) (Revised by Wolf Lammen, 30-Apr-2018.)
Hypotheses
Ref Expression
sbie.1 xψ
sbie.2 (x = y → (φψ))
Assertion
Ref Expression
sbie ([y / x]φψ)

Proof of Theorem sbie
StepHypRef Expression
1 sbie.1 . . 3 xψ
21nfri 1393 . 2 (ψxψ)
3 sbie.2 . 2 (x = y → (φψ))
42, 3sbieh 1655 1 ([y / x]φψ)
 Colors of variables: wff set class Syntax hints:   → wi 4   ↔ wb 98  Ⅎwnf 1329  [wsb 1627 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-gen 1318  ax-ie1 1363  ax-ie2 1364  ax-4 1381  ax-i9 1404  ax-ial 1409 This theorem depends on definitions:  df-bi 110  df-nf 1330  df-sb 1628 This theorem is referenced by:  cbveu  1906  mo4f  1942  bm1.1  2007  eqsb3lem  2122  clelsb3  2124  clelsb4  2125  cbvab  2142  cbvralf  2505  cbvrexf  2506  cbvreu  2509  sbralie  2524  cbvrab  2533  reu2  2706  nfcdeq  2738  sbcco2  2763  sbcie2g  2773  sbcralt  2811  sbcrext  2812  sbcralg  2813  sbcrexg  2814  sbcreug  2815  sbcel12g  2842  sbceqg  2843  cbvralcsf  2885  cbvrexcsf  2886  cbvreucsf  2887  cbvrabcsf  2888  sbss  3308  sbcbrg  3787  cbvopab1  3804  cbvmpt  3825  tfis2f  4234  cbviota  4799  relelfvdm  5130  nfvres  5131  cbvriota  5402
 Copyright terms: Public domain W3C validator