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

Theorem sbiev 2321
Description: Conversion of implicit substitution to explicit substitution. Version of sbie 2537 with a disjoint variable condition, not requiring ax-13 2381. See sbievw 2094 for a version with a disjoint variable condition requiring fewer axioms. (Contributed by Wolf Lammen, 18-Jan-2023.) Remove dependence on ax-10 2136 and shorten proof. (Revised by BJ, 18-Jul-2023.)
Hypotheses
Ref Expression
sbiev.1 𝑥𝜓
sbiev.2 (𝑥 = 𝑦 → (𝜑𝜓))
Assertion
Ref Expression
sbiev ([𝑦 / 𝑥]𝜑𝜓)
Distinct variable group:   𝑥,𝑦
Allowed substitution hints:   𝜑(𝑥,𝑦)   𝜓(𝑥,𝑦)

Proof of Theorem sbiev
StepHypRef Expression
1 sb6 2084 . 2 ([𝑦 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑦𝜑))
2 sbiev.1 . . 3 𝑥𝜓
3 sbiev.2 . . 3 (𝑥 = 𝑦 → (𝜑𝜓))
42, 3equsalv 2258 . 2 (∀𝑥(𝑥 = 𝑦𝜑) ↔ 𝜓)
51, 4bitri 276 1 ([𝑦 / 𝑥]𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wal 1526  wnf 1775  [wsb 2060
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-12 2167
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-nf 1776  df-sb 2061
This theorem is referenced by:  sbiedw  2323  sbiedwOLD  2324  sbco2v  2343  mo4f  2644  cbvmow  2681  cbveuw  2683  cbvabw  2887  cbvralfw  3435  cbvreuw  3441  cbvrabw  3487  reu2  3713  rmo4f  3723  sbcralt  3852  sbcreu  3856  sbcel12  4357  sbceqg  4358  sbcbr123  5111  cbvmptf  5156  wfis2fg  6178  tfis2f  7559  tfinds  7563  clwwlknonclwlknonf1o  28068  dlwwlknondlwlknonf1o  28071  funcnv4mpt  30342  nn0min  30463  ballotlemodife  31654  setinds2f  32921  frpoins2fg  32979  frins2fg  32986  scottabf  40453
  Copyright terms: Public domain W3C validator