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

Theorem sbie 2300
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 2260 . . 3 [𝑦 / 𝑥]𝑥 = 𝑦
2 sbie.2 . . . 4 (𝑥 = 𝑦 → (𝜑𝜓))
32sbimi 1836 . . 3 ([𝑦 / 𝑥]𝑥 = 𝑦 → [𝑦 / 𝑥](𝜑𝜓))
41, 3ax-mp 5 . 2 [𝑦 / 𝑥](𝜑𝜓)
5 sbie.1 . . . 4 𝑥𝜓
65sbf 2272 . . 3 ([𝑦 / 𝑥]𝜓𝜓)
76sblbis 2296 . 2 ([𝑦 / 𝑥](𝜑𝜓) ↔ ([𝑦 / 𝑥]𝜑𝜓))
84, 7mpbi 218 1 ([𝑦 / 𝑥]𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wnf 1698  [wsb 1830
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885  ax-10 1966  ax-12 1983  ax-13 2137
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-ex 1695  df-nf 1699  df-sb 1831
This theorem is referenced by:  sbied  2301  equsb3lem  2323  elsb3  2326  elsb4  2327  cbveu  2397  mo4f  2408  2mos  2444  eqsb3lem  2618  clelsb3  2620  cbvab  2637  cbvralf  3045  cbvreu  3049  sbralie  3064  cbvrab  3075  reu2  3265  nfcdeq  3303  sbcco2  3330  sbcie2g  3340  sbcralt  3381  sbcreu  3386  cbvralcsf  3435  cbvreucsf  3437  cbvrabcsf  3438  sbcel12  3838  sbceqg  3839  sbss  3937  sbcbr123  4534  cbvopab1  4553  cbvmpt  4575  wfis2fg  5524  cbviota  5663  cbvriota  6403  tfis2f  6828  tfinds  6832  nd1  9168  nd2  9169  clelsb3f  28496  rmo4fOLD  28512  rmo4f  28513  funcnv4mpt  28645  nn0min  28753  ballotlemodife  29697  bnj1321  30198  setinds2f  30774  frins2fg  30834  bj-clelsb3  31877  bj-sbeqALT  31922  prtlem5  33056  sbcrexgOLD  36261  sbcel12gOLD  37676
  Copyright terms: Public domain W3C validator