![]() |
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 2092. (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 2262 | . 2 ⊢ (Ⅎ𝑥𝜑 → ([𝑦 / 𝑥]𝜑 ↔ 𝜑)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 Ⅎwnf 1786 [wsb 2068 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-12 2172 |
This theorem depends on definitions: df-bi 206 df-ex 1783 df-nf 1787 df-sb 2069 |
This theorem is referenced by: sbf2 2264 sbh 2265 nfs1f 2267 sbrimOLD 2302 sblim 2303 sbrbif 2308 sb8f 2350 sb6x 2463 sbequ5 2464 sbequ6 2465 sb2ae 2499 sbie 2505 sbid2 2511 sbabel 2942 sbabelOLD 2943 sbhypf 3510 nfcdeq 3740 mo5f 31459 suppss2f 31595 fmptdF 31614 disjdsct 31658 esumpfinvalf 32715 bj-sbf3 35333 bj-sbf4 35334 ellimcabssub0 43932 2reu8i 45419 ichf 45716 |
Copyright terms: Public domain | W3C validator |