Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  sbie Structured version   Visualization version   GIF version

Theorem sbie 2396
 Description: Conversion of implicit substitution to explicit substitution. (Contributed by NM, 30-Jun-1994.) (Revised by Mario Carneiro, 4-Oct-2016.) (Proof shortened by Wolf Lammen, 13-Jul-2019.)
Hypotheses
Ref Expression
sbie.1 𝑥𝜓
sbie.2 (𝑥 = 𝑦 → (𝜑𝜓))
Assertion
Ref Expression
sbie ([𝑦 / 𝑥]𝜑𝜓)

Proof of Theorem sbie
StepHypRef Expression
1 equsb1 2356 . . 3 [𝑦 / 𝑥]𝑥 = 𝑦
2 sbie.2 . . . 4 (𝑥 = 𝑦 → (𝜑𝜓))
32sbimi 1873 . . 3 ([𝑦 / 𝑥]𝑥 = 𝑦 → [𝑦 / 𝑥](𝜑𝜓))
41, 3ax-mp 5 . 2 [𝑦 / 𝑥](𝜑𝜓)
5 sbie.1 . . . 4 𝑥𝜓
65sbf 2368 . . 3 ([𝑦 / 𝑥]𝜓𝜓)
76sblbis 2392 . 2 ([𝑦 / 𝑥](𝜑𝜓) ↔ ([𝑦 / 𝑥]𝜑𝜓))
84, 7mpbi 219 1 ([𝑦 / 𝑥]𝜑𝜓)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195  Ⅎwnf 1699  [wsb 1867 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-12 2034  ax-13 2234 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868 This theorem is referenced by:  sbied  2397  equsb3lem  2419  elsb3  2422  elsb4  2423  cbveu  2493  mo4f  2504  2mos  2540  eqsb3lem  2714  clelsb3  2716  cbvab  2733  cbvralf  3141  cbvreu  3145  sbralie  3160  cbvrab  3171  reu2  3361  nfcdeq  3399  sbcco2  3426  sbcie2g  3436  sbcralt  3477  sbcreu  3482  cbvralcsf  3531  cbvreucsf  3533  cbvrabcsf  3534  sbcel12  3935  sbceqg  3936  sbss  4034  sbcbr123  4636  cbvopab1  4655  cbvmpt  4677  wfis2fg  5634  cbviota  5773  cbvriota  6521  tfis2f  6947  tfinds  6951  nd1  9288  nd2  9289  clelsb3f  28704  rmo4fOLD  28720  rmo4f  28721  funcnv4mpt  28853  nn0min  28954  ballotlemodife  29886  bnj1321  30349  setinds2f  30928  frins2fg  30988  bj-clelsb3  32042  bj-sbeqALT  32087  prtlem5  33162  sbcrexgOLD  36367  sbcel12gOLD  37775
 Copyright terms: Public domain W3C validator