![]() |
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 2517 with an additional disjoint variable condition on 𝑥, 𝑧 but not requiring ax-13 2366. (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 2181 | . . 3 ⊢ (𝜑 → ∀𝑧𝜑) |
3 | 2 | hbsbw 2162 | . 2 ⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑧[𝑦 / 𝑥]𝜑) |
4 | 3 | nf5i 2135 | 1 ⊢ Ⅎ𝑧[𝑦 / 𝑥]𝜑 |
Colors of variables: wff setvar class |
Syntax hints: Ⅎwnf 1778 [wsb 2060 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-10 2130 ax-11 2147 ax-12 2164 |
This theorem depends on definitions: df-bi 206 df-ex 1775 df-nf 1779 df-sb 2061 |
This theorem is referenced by: hbsbwOLD 2320 sbco2v 2321 2sb8ef 2347 sb8euv 2588 2mo 2639 nfcriiOLD 2891 cbvralfwOLD 3315 cbvreuwOLD 3407 cbvrabw 3462 cbvrabcsfw 3933 cbvopab1 5217 cbvmptf 5251 ralxpf 5843 cbviotaw 6501 cbvriotaw 7379 dfoprab4f 8052 mo5f 32260 ax11-pm2 36236 dfich2 46711 ichbi12i 46713 |
Copyright terms: Public domain | W3C validator |