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

Theorem sbiev 2314
Description: Conversion of implicit substitution to explicit substitution. Version of sbie 2507 with a disjoint variable condition, not requiring ax-13 2377. See sbievw 2093 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 2141 and shorten proof. (Revised by BJ, 18-Jul-2023.) (Proof shortened by SN, 24-Jul-2025.)
Hypotheses
Ref Expression
sbiev.1 𝑥𝜓
sbiev.2 (𝑥 = 𝑦 → (𝜑𝜓))
Assertion
Ref Expression
sbiev ([𝑦 / 𝑥]𝜑𝜓)
Distinct variable group:   𝑥,𝑦
Allowed substitution hints:   𝜑(𝑥,𝑦)   𝜓(𝑥,𝑦)

Proof of Theorem sbiev
StepHypRef Expression
1 sbiev.2 . . 3 (𝑥 = 𝑦 → (𝜑𝜓))
21sbbiiev 2092 . 2 ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜓)
3 sbiev.1 . . 3 𝑥𝜓
43sbf 2271 . 2 ([𝑦 / 𝑥]𝜓𝜓)
52, 4bitri 275 1 ([𝑦 / 𝑥]𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wnf 1783  [wsb 2064
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 1967  ax-7 2007  ax-12 2177
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-nf 1784  df-sb 2065
This theorem is referenced by:  sbiedw  2316  sbco2v  2332  mo4f  2567  cbvreuwOLD  3415  cbvrabwOLD  3474  reu2  3731  rmo4f  3741  sbcralt  3872  sbcreu  3876  sbcel12  4411  sbceqg  4412  sbcbr123  5197  cbvmptf  5251  frpoins2fg  6365  wfis2fgOLD  6378  tfis2f  7877  tfinds  7881  frins2f  9793  clwwlknonclwlknonf1o  30381  dlwwlknondlwlknonf1o  30384  funcnv4mpt  32679  nn0min  32822  ballotlemodife  34500  bnj1321  35041  setinds2f  35780  bj-sbeqALT  36901  scottabf  44259
  Copyright terms: Public domain W3C validator