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 2565 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 2342 | . . . 4 ⊢ Ⅎ𝑧∀𝑥(𝑥 = 𝑤 → 𝜑) |
7 | 2, 6 | nfim 1897 | . . 3 ⊢ Ⅎ𝑧(𝑤 = 𝑦 → ∀𝑥(𝑥 = 𝑤 → 𝜑)) |
8 | 7 | nfal 2342 | . 2 ⊢ Ⅎ𝑧∀𝑤(𝑤 = 𝑦 → ∀𝑥(𝑥 = 𝑤 → 𝜑)) |
9 | 1, 8 | nfxfr 1853 | 1 ⊢ Ⅎ𝑧[𝑦 / 𝑥]𝜑 |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1535 Ⅎwnf 1784 [wsb 2069 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-10 2145 ax-11 2161 ax-12 2177 |
This theorem depends on definitions: df-bi 209 df-an 399 df-ex 1781 df-nf 1785 df-sb 2070 |
This theorem is referenced by: hbsbw 2351 sbco2v 2352 2sb8ev 2375 sb8euv 2685 2mo 2733 nfcrii 2970 cbvralfw 3437 cbvreuw 3443 cbvrabw 3489 cbvrabcsfw 3924 cbvopab1 5139 cbvmptf 5165 ralxpf 5717 cbviotaw 6321 cbvriotaw 7123 dfoprab4f 7754 mo5f 30253 ax11-pm2 34159 dfich2 43662 dfich2ai 43663 ichbi12i 43667 |
Copyright terms: Public domain | W3C validator |