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

Theorem sbiev 2309
Description: Conversion of implicit substitution to explicit substitution. Version of sbie 2506 with a disjoint variable condition, not requiring ax-13 2372. See sbievw 2095 for a version with a disjoint variable condition requiring fewer axioms. (Contributed by NM, 30-Jun-1994.) (Revised by Wolf Lammen, 18-Jan-2023.) Remove dependence on ax-10 2137 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 2088 . 2 ([𝑦 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑦𝜑))
2 sbiev.1 . . 3 𝑥𝜓
3 sbiev.2 . . 3 (𝑥 = 𝑦 → (𝜑𝜓))
42, 3equsalv 2259 . 2 (∀𝑥(𝑥 = 𝑦𝜑) ↔ 𝜓)
51, 4bitri 274 1 ([𝑦 / 𝑥]𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wal 1537  wnf 1786  [wsb 2067
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-12 2171
This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-nf 1787  df-sb 2068
This theorem is referenced by:  sbiedw  2310  sbco2v  2327  mo4f  2567  cbvmowOLD  2604  cbveuwOLD  2608  cbvabwOLD  2813  cbvralfwOLD  3369  cbvreuwOLD  3377  cbvrabw  3424  reu2  3660  rmo4f  3670  sbcralt  3805  sbcreu  3809  sbcel12  4342  sbceqg  4343  sbcbr123  5128  cbvmptf  5183  frpoins2fg  6247  wfis2fgOLD  6260  tfis2f  7702  tfinds  7706  frins2f  9511  clwwlknonclwlknonf1o  28726  dlwwlknondlwlknonf1o  28729  funcnv4mpt  31006  nn0min  31134  ballotlemodife  32464  bnj1321  33007  setinds2f  33755  bj-sbeqALT  35085  scottabf  41858
  Copyright terms: Public domain W3C validator