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

Theorem sbiev 2317
Description: Conversion of implicit substitution to explicit substitution. Version of sbie 2507 with a disjoint variable condition, not requiring ax-13 2373. See sbievw 2103 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 2145 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 2095 . 2 ([𝑦 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑦𝜑))
2 sbiev.1 . . 3 𝑥𝜓
3 sbiev.2 . . 3 (𝑥 = 𝑦 → (𝜑𝜓))
42, 3equsalv 2268 . 2 (∀𝑥(𝑥 = 𝑦𝜑) ↔ 𝜓)
51, 4bitri 278 1 ([𝑦 / 𝑥]𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wal 1540  wnf 1790  [wsb 2074
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-12 2179
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1787  df-nf 1791  df-sb 2075
This theorem is referenced by:  sbiedw  2318  sbiedwOLD  2319  sbco2v  2335  mo4f  2568  cbvmowOLD  2606  cbveuwOLD  2610  cbvabwOLD  2809  cbvralfwOLD  3337  cbvreuw  3343  cbvrabw  3392  reu2  3625  rmo4f  3635  sbcralt  3764  sbcreu  3768  sbcel12  4299  sbceqg  4300  sbcbr123  5085  cbvmptf  5130  wfis2fg  6167  tfis2f  7592  tfinds  7596  clwwlknonclwlknonf1o  28302  dlwwlknondlwlknonf1o  28305  funcnv4mpt  30584  nn0min  30712  ballotlemodife  32037  bnj1321  32581  setinds2f  33332  frpoins2fg  33390  frins2fg  33400  bj-sbeqALT  34732  scottabf  41423
  Copyright terms: Public domain W3C validator