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

Theorem sbie 2503
Description: Conversion of implicit substitution to explicit substitution. For versions requiring disjoint variables, but fewer axioms, see sbiev 2311 and sbievw 2089. Usage of this theorem is discouraged because it depends on ax-13 2373. (Contributed by NM, 30-Jun-1994.) (Revised by Mario Carneiro, 4-Oct-2016.) (Proof shortened by Wolf Lammen, 13-Jul-2019.) (New usage is discouraged.)
Hypotheses
Ref Expression
sbie.1 𝑥𝜓
sbie.2 (𝑥 = 𝑦 → (𝜑𝜓))
Assertion
Ref Expression
sbie ([𝑦 / 𝑥]𝜑𝜓)

Proof of Theorem sbie
StepHypRef Expression
1 equsb1 2492 . . 3 [𝑦 / 𝑥]𝑥 = 𝑦
2 sbie.2 . . . 4 (𝑥 = 𝑦 → (𝜑𝜓))
32sbimi 2070 . . 3 ([𝑦 / 𝑥]𝑥 = 𝑦 → [𝑦 / 𝑥](𝜑𝜓))
41, 3ax-mp 5 . 2 [𝑦 / 𝑥](𝜑𝜓)
5 sbie.1 . . . 4 𝑥𝜓
65sbf 2267 . . 3 ([𝑦 / 𝑥]𝜓𝜓)
76sblbis 2306 . 2 ([𝑦 / 𝑥](𝜑𝜓) ↔ ([𝑦 / 𝑥]𝜑𝜓))
84, 7mpbi 230 1 ([𝑦 / 𝑥]𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wnf 1778  [wsb 2060
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1963  ax-7 2003  ax-10 2137  ax-12 2173  ax-13 2373
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-ex 1775  df-nf 1779  df-sb 2061
This theorem is referenced by:  sbied  2504  2sbiev  2506  cbvmo  2600  cbveu  2603  cbvab  2810  clelsb2OLD  2866  cbvralf  3356  cbvreu  3424  cbvrab  3476  nfcdeq  3786  cbvralcsf  3953  cbvreucsf  3955  cbvrabcsf  3956  cbvopab1g  5226  cbvmptfg  5260  cbviota  6521  cbvriota  7396  nd1  10619  nd2  10620  sbcrexgOLD  42734
  Copyright terms: Public domain W3C validator