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

Theorem sbie 2497
Description: Conversion of implicit substitution to explicit substitution. For versions requiring disjoint variables, but fewer axioms, see sbiev 2304 and sbievw 2088. Usage of this theorem is discouraged because it depends on ax-13 2367. (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 2486 . . 3 [𝑦 / 𝑥]𝑥 = 𝑦
2 sbie.2 . . . 4 (𝑥 = 𝑦 → (𝜑𝜓))
32sbimi 2070 . . 3 ([𝑦 / 𝑥]𝑥 = 𝑦 → [𝑦 / 𝑥](𝜑𝜓))
41, 3ax-mp 5 . 2 [𝑦 / 𝑥](𝜑𝜓)
5 sbie.1 . . . 4 𝑥𝜓
65sbf 2258 . . 3 ([𝑦 / 𝑥]𝜓𝜓)
76sblbis 2299 . 2 ([𝑦 / 𝑥](𝜑𝜓) ↔ ([𝑦 / 𝑥]𝜑𝜓))
84, 7mpbi 229 1 ([𝑦 / 𝑥]𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  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 1964  ax-7 2004  ax-10 2130  ax-12 2167  ax-13 2367
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-ex 1775  df-nf 1779  df-sb 2061
This theorem is referenced by:  sbied  2498  2sbiev  2500  cbvmo  2595  cbveu  2599  cbvab  2804  clelsb2OLD  2858  cbvralf  3352  cbvreu  3420  cbvrab  3469  nfcdeq  3771  cbvralcsf  3935  cbvreucsf  3937  cbvrabcsf  3938  cbvopab1g  5218  cbvmptfg  5252  cbviota  6504  cbvriota  7384  nd1  10604  nd2  10605  sbcrexgOLD  42199
  Copyright terms: Public domain W3C validator