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

Theorem sbie 2412
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 2372 . . 3 [𝑦 / 𝑥]𝑥 = 𝑦
2 sbie.2 . . . 4 (𝑥 = 𝑦 → (𝜑𝜓))
32sbimi 1888 . . 3 ([𝑦 / 𝑥]𝑥 = 𝑦 → [𝑦 / 𝑥](𝜑𝜓))
41, 3ax-mp 5 . 2 [𝑦 / 𝑥](𝜑𝜓)
5 sbie.1 . . . 4 𝑥𝜓
65sbf 2384 . . 3 ([𝑦 / 𝑥]𝜓𝜓)
76sblbis 2408 . 2 ([𝑦 / 𝑥](𝜑𝜓) ↔ ([𝑦 / 𝑥]𝜑𝜓))
84, 7mpbi 220 1 ([𝑦 / 𝑥]𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wnf 1705  [wsb 1882
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-10 2021  ax-12 2049  ax-13 2250
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-ex 1702  df-nf 1707  df-sb 1883
This theorem is referenced by:  sbied  2413  equsb3lem  2435  elsb3  2438  elsb4  2439  cbveu  2509  mo4f  2520  2mos  2556  eqsb3lem  2730  clelsb3  2732  cbvab  2749  cbvralf  3158  cbvreu  3162  sbralie  3177  cbvrab  3189  reu2  3381  nfcdeq  3419  sbcco2  3446  sbcie2g  3456  sbcralt  3497  sbcreu  3502  cbvralcsf  3551  cbvreucsf  3553  cbvrabcsf  3554  sbcel12  3960  sbceqg  3961  sbss  4061  sbcbr123  4671  cbvopab1  4690  cbvmpt  4714  wfis2fg  5679  cbviota  5818  cbvriota  6576  tfis2f  7003  tfinds  7007  nd1  9354  nd2  9355  clelsb3f  29160  rmo4fOLD  29176  rmo4f  29177  funcnv4mpt  29304  nn0min  29400  ballotlemodife  30332  bnj1321  30795  setinds2f  31373  frins2fg  31433  bj-clelsb3  32468  bj-sbeqALT  32515  prtlem5  33591  sbcrexgOLD  36796  sbcel12gOLD  38203
  Copyright terms: Public domain W3C validator