![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nfsbv | Structured version Visualization version GIF version |
Description: If 𝑧 is not free in 𝜑, it is not free in [𝑦 / 𝑥]𝜑 when 𝑧 is distinct from 𝑥 and 𝑦. Version of nfsb 2542 requiring more disjoint variables, but fewer axioms. (Contributed by Mario Carneiro, 11-Aug-2016.) (Revised by Wolf Lammen, 7-Feb-2023.) Remove disjoint variable condition on 𝑥, 𝑦. (Revised by Steven Nguyen, 13-Aug-2023.) |
Ref | Expression |
---|---|
nfsbv.nf | ⊢ Ⅎ𝑧𝜑 |
Ref | Expression |
---|---|
nfsbv | ⊢ Ⅎ𝑧[𝑦 / 𝑥]𝜑 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-sb 2070 | . 2 ⊢ ([𝑦 / 𝑥]𝜑 ↔ ∀𝑤(𝑤 = 𝑦 → ∀𝑥(𝑥 = 𝑤 → 𝜑))) | |
2 | nfv 1915 | . . . 4 ⊢ Ⅎ𝑧 𝑤 = 𝑦 | |
3 | nfv 1915 | . . . . . 6 ⊢ Ⅎ𝑧 𝑥 = 𝑤 | |
4 | nfsbv.nf | . . . . . 6 ⊢ Ⅎ𝑧𝜑 | |
5 | 3, 4 | nfim 1897 | . . . . 5 ⊢ Ⅎ𝑧(𝑥 = 𝑤 → 𝜑) |
6 | 5 | nfal 2331 | . . . 4 ⊢ Ⅎ𝑧∀𝑥(𝑥 = 𝑤 → 𝜑) |
7 | 2, 6 | nfim 1897 | . . 3 ⊢ Ⅎ𝑧(𝑤 = 𝑦 → ∀𝑥(𝑥 = 𝑤 → 𝜑)) |
8 | 7 | nfal 2331 | . 2 ⊢ Ⅎ𝑧∀𝑤(𝑤 = 𝑦 → ∀𝑥(𝑥 = 𝑤 → 𝜑)) |
9 | 1, 8 | nfxfr 1854 | 1 ⊢ Ⅎ𝑧[𝑦 / 𝑥]𝜑 |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1536 Ⅎwnf 1785 [wsb 2069 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-10 2142 ax-11 2158 ax-12 2175 |
This theorem depends on definitions: df-bi 210 df-an 400 df-ex 1782 df-nf 1786 df-sb 2070 |
This theorem is referenced by: hbsbwOLD 2340 sbco2v 2341 2sb8ev 2364 sb8euv 2660 2mo 2710 nfcriiOLD 2949 cbvralfwOLD 3383 cbvreuw 3389 cbvrabw 3437 cbvrabcsfw 3869 cbvopab1 5103 cbvmptf 5129 ralxpf 5681 cbviotaw 6290 cbvriotaw 7102 dfoprab4f 7736 mo5f 30260 ax11-pm2 34274 dfich2 43975 ichbi12i 43977 |
Copyright terms: Public domain | W3C validator |