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

Theorem sbie 1671
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 1409 . 2 (ψxψ)
3 sbie.2 . 2 (x = y → (φψ))
42, 3sbieh 1670 1 ([y / x]φψ)
Colors of variables: wff set class
Syntax hints:  wi 4  wb 98  wnf 1346  [wsb 1642
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-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-4 1397  ax-i9 1420  ax-ial 1424
This theorem depends on definitions:  df-bi 110  df-nf 1347  df-sb 1643
This theorem is referenced by:  cbveu  1921  mo4f  1957  bm1.1  2022  eqsb3lem  2137  clelsb3  2139  clelsb4  2140  cbvab  2157  cbvralf  2521  cbvrexf  2522  cbvreu  2525  sbralie  2540  cbvrab  2549  reu2  2723  nfcdeq  2755  sbcco2  2780  sbcie2g  2790  sbcralt  2828  sbcrext  2829  sbcralg  2830  sbcrexg  2831  sbcreug  2832  sbcel12g  2859  sbceqg  2860  cbvralcsf  2902  cbvrexcsf  2903  cbvreucsf  2904  cbvrabcsf  2905  sbss  3323  sbcbrg  3804  cbvopab1  3821  cbvmpt  3842  tfis2f  4250  cbviota  4815  relelfvdm  5148  nfvres  5149  cbvriota  5421
  Copyright terms: Public domain W3C validator