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

Theorem sbie 1674
 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 1412 . 2 (𝜓 → ∀𝑥𝜓)
3 sbie.2 . 2 (𝑥 = 𝑦 → (𝜑𝜓))
42, 3sbieh 1673 1 ([𝑦 / 𝑥]𝜑𝜓)
 Colors of variables: wff set class Syntax hints:   → wi 4   ↔ wb 98  Ⅎwnf 1349  [wsb 1645 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 1336  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-4 1400  ax-i9 1423  ax-ial 1427 This theorem depends on definitions:  df-bi 110  df-nf 1350  df-sb 1646 This theorem is referenced by:  cbveu  1924  mo4f  1960  bm1.1  2025  eqsb3lem  2140  clelsb3  2142  clelsb4  2143  cbvab  2160  cbvralf  2527  cbvrexf  2528  cbvreu  2531  sbralie  2546  cbvrab  2555  reu2  2729  nfcdeq  2761  sbcco2  2786  sbcie2g  2796  sbcralt  2834  sbcrext  2835  sbcralg  2836  sbcreug  2838  sbcel12g  2865  sbceqg  2866  cbvralcsf  2908  cbvrexcsf  2909  cbvreucsf  2910  cbvrabcsf  2911  sbss  3329  sbcbrg  3813  cbvopab1  3830  cbvmpt  3851  tfis2f  4307  cbviota  4872  relelfvdm  5205  nfvres  5206  cbvriota  5478
 Copyright terms: Public domain W3C validator