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 2505 with a disjoint variable condition, not requiring ax-13 2371. See sbievw 2096 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 2138 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 2089 . 2 ([𝑦 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑦𝜑))
2 sbiev.1 . . 3 𝑥𝜓
3 sbiev.2 . . 3 (𝑥 = 𝑦 → (𝜑𝜓))
42, 3equsalv 2259 . 2 (∀𝑥(𝑥 = 𝑦𝜑) ↔ 𝜓)
51, 4bitri 275 1 ([𝑦 / 𝑥]𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wal 1540  wnf 1786  [wsb 2068
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 1914  ax-6 1972  ax-7 2012  ax-12 2172
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-nf 1787  df-sb 2069
This theorem is referenced by:  sbiedw  2310  sbco2v  2327  mo4f  2566  cbvmowOLD  2603  cbveuwOLD  2607  cbvabwOLD  2812  cbvralfwOLD  3307  cbvreuwOLD  3392  cbvrabw  3442  reu2  3688  rmo4f  3698  sbcralt  3833  sbcreu  3837  sbcel12  4373  sbceqg  4374  sbcbr123  5164  cbvmptf  5219  frpoins2fg  6303  wfis2fgOLD  6316  tfis2f  7797  tfinds  7801  frins2f  9696  clwwlknonclwlknonf1o  29348  dlwwlknondlwlknonf1o  29351  funcnv4mpt  31627  nn0min  31758  ballotlemodife  33137  bnj1321  33679  setinds2f  34393  bj-sbeqALT  35396  scottabf  42594
  Copyright terms: Public domain W3C validator