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

Theorem sbie 2395
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 2355 . . 3 [𝑦 / 𝑥]𝑥 = 𝑦
2 sbie.2 . . . 4 (𝑥 = 𝑦 → (𝜑𝜓))
32sbimi 1872 . . 3 ([𝑦 / 𝑥]𝑥 = 𝑦 → [𝑦 / 𝑥](𝜑𝜓))
41, 3ax-mp 5 . 2 [𝑦 / 𝑥](𝜑𝜓)
5 sbie.1 . . . 4 𝑥𝜓
65sbf 2367 . . 3 ([𝑦 / 𝑥]𝜓𝜓)
76sblbis 2391 . 2 ([𝑦 / 𝑥](𝜑𝜓) ↔ ([𝑦 / 𝑥]𝜑𝜓))
84, 7mpbi 218 1 ([𝑦 / 𝑥]𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wnf 1698  [wsb 1866
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-12 2033  ax-13 2233
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867
This theorem is referenced by:  sbied  2396  equsb3lem  2418  elsb3  2421  elsb4  2422  cbveu  2492  mo4f  2503  2mos  2539  eqsb3lem  2713  clelsb3  2715  cbvab  2732  cbvralf  3140  cbvreu  3144  sbralie  3159  cbvrab  3170  reu2  3360  nfcdeq  3398  sbcco2  3425  sbcie2g  3435  sbcralt  3476  sbcreu  3481  cbvralcsf  3530  cbvreucsf  3532  cbvrabcsf  3533  sbcel12  3934  sbceqg  3935  sbss  4033  sbcbr123  4630  cbvopab1  4649  cbvmpt  4671  wfis2fg  5620  cbviota  5759  cbvriota  6499  tfis2f  6924  tfinds  6928  nd1  9265  nd2  9266  clelsb3f  28510  rmo4fOLD  28526  rmo4f  28527  funcnv4mpt  28659  nn0min  28760  ballotlemodife  29692  bnj1321  30155  setinds2f  30734  frins2fg  30794  bj-clelsb3  31838  bj-sbeqALT  31883  prtlem5  32958  sbcrexgOLD  36163  sbcel12gOLD  37571
  Copyright terms: Public domain W3C validator