Description: Substitution for a variable not free in a wff does not affect it. For a version requiring disjoint variables but fewer axioms, see sbv . (Contributed by NM, 14-May-1993) (Revised by Mario Carneiro, 4-Oct-2016)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | sbf.1 | |- F/ x ph |
|
| Assertion | sbf | |- ( [ y / x ] ph <-> ph ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | sbf.1 | |- F/ x ph |
|
| 2 | sbft | |- ( F/ x ph -> ( [ y / x ] ph <-> ph ) ) |
|
| 3 | 1 2 | ax-mp | |- ( [ y / x ] ph <-> ph ) |