![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nfsb | Structured version Visualization version GIF version |
Description: If 𝑧 is not free in 𝜑, then it is not free in [𝑦 / 𝑥]𝜑 when 𝑦 and 𝑧 are distinct. See nfsbv 2324 for a version with an additional disjoint variable condition on 𝑥, 𝑧 but not requiring ax-13 2372. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 25-Feb-2024.) Usage of this theorem is discouraged because it depends on ax-13 2372. Use nfsbv 2324 instead. (New usage is discouraged.) |
Ref | Expression |
---|---|
nfsb.1 | ⊢ Ⅎ𝑧𝜑 |
Ref | Expression |
---|---|
nfsb | ⊢ Ⅎ𝑧[𝑦 / 𝑥]𝜑 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nftru 1807 | . . 3 ⊢ Ⅎ𝑥⊤ | |
2 | nfsb.1 | . . . 4 ⊢ Ⅎ𝑧𝜑 | |
3 | 2 | a1i 11 | . . 3 ⊢ (⊤ → Ⅎ𝑧𝜑) |
4 | 1, 3 | nfsbd 2522 | . 2 ⊢ (⊤ → Ⅎ𝑧[𝑦 / 𝑥]𝜑) |
5 | 4 | mptru 1549 | 1 ⊢ Ⅎ𝑧[𝑦 / 𝑥]𝜑 |
Colors of variables: wff setvar class |
Syntax hints: ⊤wtru 1543 Ⅎ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 ax-13 2372 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-tru 1545 df-ex 1783 df-nf 1787 df-sb 2069 |
This theorem is referenced by: hbsb 2524 sb10f 2527 2sb8e 2530 sb8eu 2595 cbvralf 3357 cbvralsv 3363 cbvrexsv 3364 cbvreu 3425 cbvrab 3474 cbvreucsf 3941 cbvrabcsf 3942 cbvopab1g 5225 cbvmptfg 5259 cbviota 6506 sb8iota 6508 cbvriota 7379 2sb5nd 43321 |
Copyright terms: Public domain | W3C validator |