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

Theorem sbie 2291
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 2251 . . 3 [𝑦 / 𝑥]𝑥 = 𝑦
2 sbie.2 . . . 4 (𝑥 = 𝑦 → (𝜑𝜓))
32sbimi 1834 . . 3 ([𝑦 / 𝑥]𝑥 = 𝑦 → [𝑦 / 𝑥](𝜑𝜓))
41, 3ax-mp 5 . 2 [𝑦 / 𝑥](𝜑𝜓)
5 sbie.1 . . . 4 𝑥𝜓
65sbf 2263 . . 3 ([𝑦 / 𝑥]𝜓𝜓)
76sblbis 2287 . 2 ([𝑦 / 𝑥](𝜑𝜓) ↔ ([𝑦 / 𝑥]𝜑𝜓))
84, 7mpbi 215 1 ([𝑦 / 𝑥]𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 191  wnf 1696  [wsb 1828
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1698  ax-4 1711  ax-5 1789  ax-6 1836  ax-7 1883  ax-10 1965  ax-12 1983  ax-13 2137
This theorem depends on definitions:  df-bi 192  df-or 379  df-an 380  df-ex 1693  df-nf 1697  df-sb 1829
This theorem is referenced by:  sbied  2292  equsb3lem  2314  elsb3  2317  elsb4  2318  cbveu  2388  mo4f  2399  2mos  2435  eqsb3lem  2609  clelsb3  2611  cbvab  2628  cbvralf  3034  cbvreu  3038  sbralie  3053  cbvrab  3064  reu2  3250  nfcdeq  3288  sbcco2  3315  sbcie2g  3325  sbcralt  3364  sbcreu  3368  cbvralcsf  3417  cbvreucsf  3419  cbvrabcsf  3420  sbcel12  3812  sbceqg  3813  sbss  3906  sbcbr123  4486  cbvopab1  4505  cbvmpt  4527  wfis2fg  5468  cbviota  5602  cbvriota  6335  tfis2f  6759  tfinds  6763  nd1  9097  nd2  9098  clelsb3f  28277  rmo4fOLD  28293  rmo4f  28294  funcnv4mpt  28430  nn0min  28540  ballotlemodife  29484  bnj1321  29988  setinds2f  30576  frins2fg  30636  bj-clelsb3  31641  bj-sbeqALT  31686  prtlem5  32664  sbcrexgOLD  35868  sbcel12gOLD  37261
  Copyright terms: Public domain W3C validator