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

Theorem sbie 2555
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 2515 . . 3 [𝑦 / 𝑥]𝑥 = 𝑦
2 sbie.2 . . . 4 (𝑥 = 𝑦 → (𝜑𝜓))
32sbimi 2055 . . 3 ([𝑦 / 𝑥]𝑥 = 𝑦 → [𝑦 / 𝑥](𝜑𝜓))
41, 3ax-mp 5 . 2 [𝑦 / 𝑥](𝜑𝜓)
5 sbie.1 . . . 4 𝑥𝜓
65sbf 2527 . . 3 ([𝑦 / 𝑥]𝜓𝜓)
76sblbis 2551 . 2 ([𝑦 / 𝑥](𝜑𝜓) ↔ ([𝑦 / 𝑥]𝜑𝜓))
84, 7mpbi 220 1 ([𝑦 / 𝑥]𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wnf 1856  [wsb 2049
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-10 2174  ax-12 2203  ax-13 2408
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 829  df-ex 1853  df-nf 1858  df-sb 2050
This theorem is referenced by:  sbied  2556  equsb3lem  2579  elsb3lem  2582  elsb3OLD  2584  elsb4lem  2585  elsb4OLD  2587  cbveu  2654  mo4f  2665  2mos  2701  eqsb3lem  2876  clelsb3  2878  cbvab  2895  clelsb3f  2917  cbvralf  3314  cbvreu  3318  sbralie  3333  cbvrab  3348  reu2  3547  nfcdeq  3585  sbcco2  3612  sbcie2g  3622  sbcralt  3661  sbcreu  3665  cbvralcsf  3715  cbvreucsf  3717  cbvrabcsf  3718  sbcel12  4128  sbceqg  4129  sbss  4224  sbcbr123  4841  cbvopab1  4858  cbvmpt  4884  wfis2fg  5861  cbviota  6000  cbvriota  6765  tfis2f  7203  tfinds  7207  nd1  9612  nd2  9613  clwwlknonclwlknonf1o  27550  dlwwlknondlwlknonf1o  27555  rmo4fOLD  29676  rmo4f  29677  funcnv4mpt  29811  nn0min  29908  ballotlemodife  30900  bnj1321  31434  setinds2f  32021  frins2fg  32085  bj-sbeqALT  33225  prtlem5  34669  sbcrexgOLD  37876  sbcel12gOLD  39280
  Copyright terms: Public domain W3C validator