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 2522 with an additional disjoint variable condition on 𝑥, 𝑧 but not requiring ax-13 2367. (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 2183 | . . 3 ⊢ (𝜑 → ∀𝑧𝜑) |
3 | 2 | hbsbw 2164 | . 2 ⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑧[𝑦 / 𝑥]𝜑) |
4 | 3 | nf5i 2137 | 1 ⊢ Ⅎ𝑧[𝑦 / 𝑥]𝜑 |
Colors of variables: wff setvar class |
Syntax hints: Ⅎwnf 1781 [wsb 2062 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1793 ax-4 1807 ax-5 1909 ax-6 1967 ax-7 2007 ax-10 2132 ax-11 2149 ax-12 2166 |
This theorem depends on definitions: df-bi 206 df-ex 1778 df-nf 1782 df-sb 2063 |
This theorem is referenced by: hbsbwOLD 2321 sbco2v 2322 2sb8ef 2349 sb8euv 2594 2mo 2645 nfcriiOLD 2895 cbvralfwOLD 3371 cbvreuwOLD 3379 cbvrabw 3426 cbvrabcsfw 3878 cbvopab1 5152 cbvmptf 5186 ralxpf 5759 cbviotaw 6406 cbvriotaw 7261 dfoprab4f 7916 mo5f 30865 ax11-pm2 35047 dfich2 44950 ichbi12i 44952 |
Copyright terms: Public domain | W3C validator |