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

Theorem sbie 2484
Description: Conversion of implicit substitution to explicit substitution. For a version requiring disjoint variables, but fewer axioms, see sbiev 2286. (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 2444 . . 3 [𝑦 / 𝑥]𝑥 = 𝑦
2 sbie.2 . . . 4 (𝑥 = 𝑦 → (𝜑𝜓))
32sbimi 2017 . . 3 ([𝑦 / 𝑥]𝑥 = 𝑦 → [𝑦 / 𝑥](𝜑𝜓))
41, 3ax-mp 5 . 2 [𝑦 / 𝑥](𝜑𝜓)
5 sbie.1 . . . 4 𝑥𝜓
65sbf 2456 . . 3 ([𝑦 / 𝑥]𝜓𝜓)
76sblbis 2480 . 2 ([𝑦 / 𝑥](𝜑𝜓) ↔ ([𝑦 / 𝑥]𝜑𝜓))
84, 7mpbi 222 1 ([𝑦 / 𝑥]𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wnf 1827  [wsb 2011
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-10 2135  ax-12 2163  ax-13 2334
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-ex 1824  df-nf 1828  df-sb 2012
This theorem is referenced by:  sbied  2485  equsb3vOLD  2509  elsb3OLD  2514  elsb4OLD  2517  mo4fOLD  2584  cbvmo  2637  cbveu  2638  2mos  2679  eqsb3vOLD  2886  clelsb3  2888  cbvab  2913  clelsb3fOLD  2939  cbvralf  3361  cbvreu  3365  sbralie  3380  cbvrab  3395  reu2  3606  rmo4f  3616  nfcdeq  3649  sbcco2  3676  sbcie2g  3686  sbcralt  3728  sbcreu  3732  cbvralcsf  3783  cbvreucsf  3785  cbvrabcsf  3786  sbcel12  4208  sbceqg  4209  sbss  4305  sbcbr123  4942  cbvopab1  4961  cbvmpt  4986  wfis2fg  5972  cbviota  6106  cbvriota  6895  tfis2f  7335  tfinds  7339  nd1  9746  nd2  9747  clwwlknonclwlknonf1o  27789  clwwlknonclwlknonf1oOLD  27790  dlwwlknondlwlknonf1o  27795  dlwwlknondlwlknonf1oOLD  27796  funcnv4mpt  30038  nn0min  30135  ballotlemodife  31162  bnj1321  31698  setinds2f  32276  frins2fg  32340  bj-sbeqALT  33470  prtlem5  35019  sbcrexgOLD  38319  2reu8i  42164
  Copyright terms: Public domain W3C validator