![]() |
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 2526 with an additional disjoint variable condition on 𝑥, 𝑧 but not requiring ax-13 2371. (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 2189 | . . 3 ⊢ (𝜑 → ∀𝑧𝜑) |
3 | 2 | hbsbw 2170 | . 2 ⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑧[𝑦 / 𝑥]𝜑) |
4 | 3 | nf5i 2143 | 1 ⊢ Ⅎ𝑧[𝑦 / 𝑥]𝜑 |
Colors of variables: wff setvar class |
Syntax hints: Ⅎwnf 1786 [wsb 2068 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-10 2138 ax-11 2155 ax-12 2172 |
This theorem depends on definitions: df-bi 206 df-ex 1783 df-nf 1787 df-sb 2069 |
This theorem is referenced by: hbsbwOLD 2326 sbco2v 2327 2sb8ef 2353 sb8euv 2598 2mo 2649 nfcriiOLD 2901 cbvralfwOLD 3307 cbvreuwOLD 3392 cbvrabw 3442 cbvrabcsfw 3904 cbvopab1 5185 cbvmptf 5219 ralxpf 5807 cbviotaw 6460 cbvriotaw 7327 dfoprab4f 7993 mo5f 31459 ax11-pm2 35330 dfich2 45724 ichbi12i 45726 |
Copyright terms: Public domain | W3C validator |