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

Theorem sbie 2406
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 2366 . . 3 [𝑦 / 𝑥]𝑥 = 𝑦
2 sbie.2 . . . 4 (𝑥 = 𝑦 → (𝜑𝜓))
32sbimi 1884 . . 3 ([𝑦 / 𝑥]𝑥 = 𝑦 → [𝑦 / 𝑥](𝜑𝜓))
41, 3ax-mp 5 . 2 [𝑦 / 𝑥](𝜑𝜓)
5 sbie.1 . . . 4 𝑥𝜓
65sbf 2378 . . 3 ([𝑦 / 𝑥]𝜓𝜓)
76sblbis 2402 . 2 ([𝑦 / 𝑥](𝜑𝜓) ↔ ([𝑦 / 𝑥]𝜑𝜓))
84, 7mpbi 220 1 ([𝑦 / 𝑥]𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wnf 1706  [wsb 1878
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-10 2017  ax-12 2045  ax-13 2244
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-ex 1703  df-nf 1708  df-sb 1879
This theorem is referenced by:  sbied  2407  equsb3lem  2429  elsb3  2432  elsb4  2433  cbveu  2503  mo4f  2514  2mos  2550  eqsb3lem  2725  clelsb3  2727  cbvab  2744  cbvralf  3160  cbvreu  3164  sbralie  3179  cbvrab  3193  reu2  3388  nfcdeq  3426  sbcco2  3453  sbcie2g  3463  sbcralt  3504  sbcreu  3509  cbvralcsf  3558  cbvreucsf  3560  cbvrabcsf  3561  sbcel12  3974  sbceqg  3975  sbss  4075  sbcbr123  4697  cbvopab1  4714  cbvmpt  4740  wfis2fg  5705  cbviota  5844  cbvriota  6606  tfis2f  7040  tfinds  7044  nd1  9394  nd2  9395  clelsb3f  29292  rmo4fOLD  29308  rmo4f  29309  funcnv4mpt  29444  nn0min  29541  ballotlemodife  30533  bnj1321  31069  setinds2f  31658  frins2fg  31718  bj-clelsb3  32823  bj-sbeqALT  32870  prtlem5  33963  sbcrexgOLD  37168  sbcel12gOLD  38574
  Copyright terms: Public domain W3C validator