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

Theorem sbiev 2329
 Description: Conversion of implicit substitution to explicit substitution. Version of sbie 2543 with a disjoint variable condition, not requiring ax-13 2389. See sbievw 2102 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 2144 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 2092 . 2 ([𝑦 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑦𝜑))
2 sbiev.1 . . 3 𝑥𝜓
3 sbiev.2 . . 3 (𝑥 = 𝑦 → (𝜑𝜓))
42, 3equsalv 2267 . 2 (∀𝑥(𝑥 = 𝑦𝜑) ↔ 𝜓)
51, 4bitri 277 1 ([𝑦 / 𝑥]𝜑𝜓)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 208  ∀wal 1534  Ⅎwnf 1783  [wsb 2068 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-12 2176 This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1780  df-nf 1784  df-sb 2069 This theorem is referenced by:  sbiedw  2331  sbiedwOLD  2332  sbco2v  2351  mo4f  2650  cbvmow  2687  cbveuw  2689  cbvabw  2893  cbvralfw  3440  cbvreuw  3446  cbvrabw  3492  reu2  3719  rmo4f  3729  sbcralt  3858  sbcreu  3862  sbcel12  4363  sbceqg  4364  sbcbr123  5123  cbvmptf  5168  wfis2fg  6188  tfis2f  7573  tfinds  7577  clwwlknonclwlknonf1o  28144  dlwwlknondlwlknonf1o  28147  funcnv4mpt  30417  nn0min  30540  ballotlemodife  31759  bnj1321  32303  setinds2f  33028  frpoins2fg  33086  frins2fg  33093  bj-sbeqALT  34221  scottabf  40582
 Copyright terms: Public domain W3C validator