![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > sbf | Structured version Visualization version GIF version |
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 2083. (Contributed by NM, 14-May-1993.) (Revised by Mario Carneiro, 4-Oct-2016.) |
Ref | Expression |
---|---|
sbf.1 | ⊢ Ⅎ𝑥𝜑 |
Ref | Expression |
---|---|
sbf | ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sbf.1 | . 2 ⊢ Ⅎ𝑥𝜑 | |
2 | sbft 2256 | . 2 ⊢ (Ⅎ𝑥𝜑 → ([𝑦 / 𝑥]𝜑 ↔ 𝜑)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 Ⅎwnf 1777 [wsb 2059 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-12 2166 |
This theorem depends on definitions: df-bi 206 df-ex 1774 df-nf 1778 df-sb 2060 |
This theorem is referenced by: sbf2 2258 sbh 2259 nfs1f 2261 sbrimOLD 2294 sblim 2295 sbrbif 2300 sb8f 2343 sb6x 2457 sbequ5 2458 sbequ6 2459 sb2ae 2489 sbie 2495 sbid2 2501 sbabel 2927 sbabelOLD 2928 sbhypf 3528 nfcdeq 3769 mo5f 32365 suppss2f 32505 fmptdF 32523 disjdsct 32564 esumpfinvalf 33826 bj-sbf3 36447 bj-sbf4 36448 ellimcabssub0 45143 2reu8i 46631 ichf 46927 |
Copyright terms: Public domain | W3C validator |