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

Theorem sbie 1721
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 1457 . 2 (𝜓 → ∀𝑥𝜓)
3 sbie.2 . 2 (𝑥 = 𝑦 → (𝜑𝜓))
42, 3sbieh 1720 1 ([𝑦 / 𝑥]𝜑𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wb 103  wnf 1394  [wsb 1692
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1381  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-4 1445  ax-i9 1468  ax-ial 1472
This theorem depends on definitions:  df-bi 115  df-nf 1395  df-sb 1693
This theorem is referenced by:  cbveu  1972  mo4f  2008  bm1.1  2073  eqsb3lem  2190  clelsb3  2192  clelsb4  2193  cbvab  2210  clelsb3f  2232  cbvralf  2584  cbvrexf  2585  cbvreu  2588  sbralie  2603  cbvrab  2617  reu2  2803  rmo4f  2813  nfcdeq  2837  sbcco2  2862  sbcie2g  2872  sbcralt  2915  sbcrext  2916  sbcralg  2917  sbcreug  2919  sbcel12g  2946  sbceqg  2947  cbvralcsf  2990  cbvrexcsf  2991  cbvreucsf  2992  cbvrabcsf  2993  sbss  3390  disjiun  3840  sbcbrg  3894  cbvopab1  3911  cbvmpt  3933  tfis2f  4399  cbviota  4985  relelfvdm  5336  nfvres  5337  cbvriota  5618  bezoutlemnewy  11263  bezoutlemmain  11265
  Copyright terms: Public domain W3C validator