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 𝜑, then it is not free in [𝑦 / 𝑥]𝜑 when 𝑧 is disjoint from both 𝑥 and 𝑦. Version of nfsb 2529 with an additional disjoint variable condition on 𝑥, 𝑧 but not requiring ax-13 2374. (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.) (Proof shortened by Wolf Lammen, 25-Oct-2024.) |
Ref | Expression |
---|---|
nfsbv.nf | ⊢ Ⅎ𝑧𝜑 |
Ref | Expression |
---|---|
nfsbv | ⊢ Ⅎ𝑧[𝑦 / 𝑥]𝜑 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfsbv.nf | . . . 4 ⊢ Ⅎ𝑧𝜑 | |
2 | 1 | nf5ri 2192 | . . 3 ⊢ (𝜑 → ∀𝑧𝜑) |
3 | 2 | hbsbw 2173 | . 2 ⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑧[𝑦 / 𝑥]𝜑) |
4 | 3 | nf5i 2146 | 1 ⊢ Ⅎ𝑧[𝑦 / 𝑥]𝜑 |
Colors of variables: wff setvar class |
Syntax hints: Ⅎwnf 1790 [wsb 2071 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2015 ax-10 2141 ax-11 2158 ax-12 2175 |
This theorem depends on definitions: df-bi 206 df-ex 1787 df-nf 1791 df-sb 2072 |
This theorem is referenced by: hbsbwOLD 2330 sbco2v 2331 2sb8ev 2356 sb8euv 2601 2mo 2652 nfcriiOLD 2902 cbvralfwOLD 3368 cbvreuw 3374 cbvrabw 3423 cbvrabcsfw 3881 cbvopab1 5154 cbvmptf 5188 ralxpf 5753 cbviotaw 6396 cbvriotaw 7235 dfoprab4f 7887 mo5f 30831 ax11-pm2 35013 dfich2 44877 ichbi12i 44879 |
Copyright terms: Public domain | W3C validator |