New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  sbie GIF version

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

Proof of Theorem sbie
StepHypRef Expression
1 nftru 1554 . . 3 x
2 sbie.1 . . . 4 xψ
32a1i 10 . . 3 ( ⊤ → Ⅎxψ)
4 sbie.2 . . . 4 (x = y → (φψ))
54a1i 10 . . 3 ( ⊤ → (x = y → (φψ)))
61, 3, 5sbied 2036 . 2 ( ⊤ → ([y / x]φψ))
76trud 1323 1 ([y / x]φψ)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 176   ⊤ wtru 1316  Ⅎwnf 1544  [wsb 1648 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925 This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649 This theorem is referenced by:  equsb3lem  2101  elsb3  2103  elsb4  2104  cbveu  2224  mo4f  2236  2mos  2283  bm1.1  2338  eqsb3lem  2453  clelsb3  2455  cbvab  2471  cbvralf  2829  cbvreu  2833  sbralie  2848  cbvrab  2857  reu2  3024  sbcco2  3069  sbcie2g  3079  sbcel2gv  3106  sbcralt  3118  sbcralg  3120  sbcrexg  3121  sbcreug  3122  sbcel12g  3151  sbceqg  3152  cbvralcsf  3198  cbvreucsf  3200  cbvrabcsf  3201  sbss  3659  cbviota  4344  cbvopab1  4632  sbcbrg  4685  cbvmpt  5676  fvfullfunlem1  5861
 Copyright terms: Public domain W3C validator