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

Theorem sbie 2540
Description: Conversion of implicit substitution to explicit substitution. For a version requiring disjoint variables, but fewer axioms, see sbiev 2345. (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 2500 . . 3 [𝑦 / 𝑥]𝑥 = 𝑦
2 sbie.2 . . . 4 (𝑥 = 𝑦 → (𝜑𝜓))
32sbimi 2075 . . 3 ([𝑦 / 𝑥]𝑥 = 𝑦 → [𝑦 / 𝑥](𝜑𝜓))
41, 3ax-mp 5 . 2 [𝑦 / 𝑥](𝜑𝜓)
5 sbie.1 . . . 4 𝑥𝜓
65sbf 2512 . . 3 ([𝑦 / 𝑥]𝜓𝜓)
76sblbis 2536 . 2 ([𝑦 / 𝑥](𝜑𝜓) ↔ ([𝑦 / 𝑥]𝜑𝜓))
84, 7mpbi 222 1 ([𝑦 / 𝑥]𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wnf 1884  [wsb 2069
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-10 2194  ax-12 2222  ax-13 2391
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-ex 1881  df-nf 1885  df-sb 2070
This theorem is referenced by:  sbied  2541  equsb3vOLD  2565  elsb3OLD  2570  elsb4OLD  2573  mo4fOLD  2638  cbvmo  2691  cbveu  2692  2mos  2733  eqsb3lem  2933  clelsb3  2935  cbvab  2952  clelsb3f  2974  cbvralf  3378  cbvreu  3382  sbralie  3397  cbvrab  3412  reu2  3620  rmo4f  3630  nfcdeq  3660  sbcco2  3687  sbcie2g  3697  sbcralt  3736  sbcreu  3740  cbvralcsf  3790  cbvreucsf  3792  cbvrabcsf  3793  sbcel12  4208  sbceqg  4209  sbss  4305  sbcbr123  4928  cbvopab1  4947  cbvmpt  4973  wfis2fg  5958  cbviota  6092  cbvriota  6877  tfis2f  7317  tfinds  7321  nd1  9725  nd2  9726  clwwlknonclwlknonf1o  27761  clwwlknonclwlknonf1oOLD  27762  dlwwlknondlwlknonf1o  27767  dlwwlknondlwlknonf1oOLD  27768  funcnv4mpt  30019  nn0min  30115  ballotlemodife  31106  bnj1321  31642  setinds2f  32223  frins2fg  32287  bj-sbeqALT  33417  prtlem5  34936  sbcrexgOLD  38194
  Copyright terms: Public domain W3C validator