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

Theorem sbie 1764
 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 𝑥𝜓
sbie.2 (𝑥 = 𝑦 → (𝜑𝜓))
Assertion
Ref Expression
sbie ([𝑦 / 𝑥]𝜑𝜓)

Proof of Theorem sbie
StepHypRef Expression
1 sbie.1 . . 3 𝑥𝜓
21nfri 1499 . 2 (𝜓 → ∀𝑥𝜓)
3 sbie.2 . 2 (𝑥 = 𝑦 → (𝜑𝜓))
42, 3sbieh 1763 1 ([𝑦 / 𝑥]𝜑𝜓)
 Colors of variables: wff set class Syntax hints:   → wi 4   ↔ wb 104  Ⅎwnf 1436  [wsb 1735 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 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-i9 1510  ax-ial 1514 This theorem depends on definitions:  df-bi 116  df-nf 1437  df-sb 1736 This theorem is referenced by:  sbiev  1765  cbveu  2021  mo4f  2057  bm1.1  2122  eqsb3lem  2240  clelsb3  2242  clelsb4  2243  cbvab  2261  clelsb3f  2283  cbvralf  2646  cbvrexf  2647  cbvreu  2650  sbralie  2665  cbvrab  2679  reu2  2867  rmo4f  2877  nfcdeq  2901  sbcco2  2926  sbcie2g  2937  sbcralt  2980  sbcrext  2981  sbcralg  2982  sbcreug  2984  sbcel12g  3012  sbceqg  3013  cbvralcsf  3057  cbvrexcsf  3058  cbvreucsf  3059  cbvrabcsf  3060  sbss  3466  disjiun  3919  sbcbrg  3977  cbvopab1  3996  cbvmpt  4018  tfis2f  4493  cbviota  5088  relelfvdm  5446  nfvres  5447  cbvriota  5733  bezoutlemnewy  11673  bezoutlemmain  11675
 Copyright terms: Public domain W3C validator