![]() |
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 2040. (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 2198 | . 2 ⊢ (Ⅎ𝑥𝜑 → ([𝑦 / 𝑥]𝜑 ↔ 𝜑)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 198 Ⅎwnf 1746 [wsb 2015 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-12 2106 |
This theorem depends on definitions: df-bi 199 df-ex 1743 df-nf 1747 df-sb 2016 |
This theorem is referenced by: sbf2 2200 sbh 2201 nfs1f 2204 sbbibOLD 2215 sbrim 2238 sblim 2239 sbrbif 2244 sbievOLD 2254 sb6x 2402 sbequ5 2403 sbequ6 2404 sb2ae 2457 sbie 2468 sbid2 2474 sbabel 2966 nfcdeq 3677 mo5f 30035 suppss2f 30146 fmptdF 30163 disjdsct 30197 esumpfinvalf 30985 bj-sbf3 33659 bj-sbf4 33660 ellimcabssub0 41335 2reu8i 42724 |
Copyright terms: Public domain | W3C validator |