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

Theorem sbie 2436
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 2396 . . 3 [𝑦 / 𝑥]𝑥 = 𝑦
2 sbie.2 . . . 4 (𝑥 = 𝑦 → (𝜑𝜓))
32sbimi 1943 . . 3 ([𝑦 / 𝑥]𝑥 = 𝑦 → [𝑦 / 𝑥](𝜑𝜓))
41, 3ax-mp 5 . 2 [𝑦 / 𝑥](𝜑𝜓)
5 sbie.1 . . . 4 𝑥𝜓
65sbf 2408 . . 3 ([𝑦 / 𝑥]𝜓𝜓)
76sblbis 2432 . 2 ([𝑦 / 𝑥](𝜑𝜓) ↔ ([𝑦 / 𝑥]𝜑𝜓))
84, 7mpbi 220 1 ([𝑦 / 𝑥]𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wnf 1748  [wsb 1937
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-10 2059  ax-12 2087  ax-13 2282
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-ex 1745  df-nf 1750  df-sb 1938
This theorem is referenced by:  sbied  2437  equsb3lem  2459  elsb3  2462  elsb4  2463  cbveu  2534  mo4f  2545  2mos  2581  eqsb3lem  2756  clelsb3  2758  cbvab  2775  clelsb3f  2797  cbvralf  3195  cbvreu  3199  sbralie  3214  cbvrab  3229  reu2  3427  nfcdeq  3465  sbcco2  3492  sbcie2g  3502  sbcralt  3543  sbcreu  3548  cbvralcsf  3598  cbvreucsf  3600  cbvrabcsf  3601  sbcel12  4016  sbceqg  4017  sbss  4117  sbcbr123  4739  cbvopab1  4756  cbvmpt  4782  wfis2fg  5755  cbviota  5894  cbvriota  6661  tfis2f  7097  tfinds  7101  nd1  9447  nd2  9448  rmo4fOLD  29463  rmo4f  29464  funcnv4mpt  29598  nn0min  29695  ballotlemodife  30687  bnj1321  31221  setinds2f  31808  frins2fg  31872  bj-clelsb3  32973  bj-sbeqALT  33020  prtlem5  34464  sbcrexgOLD  37666  sbcel12gOLD  39071
  Copyright terms: Public domain W3C validator