![]() |
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 2328 for a version with an additional disjoint variable condition on 𝑥, 𝑧 but not requiring ax-13 2374. (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 2374. Use nfsbv 2328 instead. (New usage is discouraged.) |
Ref | Expression |
---|---|
nfsb.1 | ⊢ Ⅎ𝑧𝜑 |
Ref | Expression |
---|---|
nfsb | ⊢ Ⅎ𝑧[𝑦 / 𝑥]𝜑 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nftru 1800 | . . 3 ⊢ Ⅎ𝑥⊤ | |
2 | nfsb.1 | . . . 4 ⊢ Ⅎ𝑧𝜑 | |
3 | 2 | a1i 11 | . . 3 ⊢ (⊤ → Ⅎ𝑧𝜑) |
4 | 1, 3 | nfsbd 2524 | . 2 ⊢ (⊤ → Ⅎ𝑧[𝑦 / 𝑥]𝜑) |
5 | 4 | mptru 1543 | 1 ⊢ Ⅎ𝑧[𝑦 / 𝑥]𝜑 |
Colors of variables: wff setvar class |
Syntax hints: ⊤wtru 1537 Ⅎwnf 1779 [wsb 2061 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1791 ax-4 1805 ax-5 1907 ax-6 1964 ax-7 2004 ax-10 2138 ax-11 2154 ax-12 2174 ax-13 2374 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-tru 1539 df-ex 1776 df-nf 1780 df-sb 2062 |
This theorem is referenced by: hbsb 2526 sb10f 2529 2sb8e 2532 sb8eu 2597 cbvralf 3357 cbvralsv 3363 cbvrexsv 3364 cbvreu 3424 cbvrab 3476 cbvreucsf 3954 cbvrabcsf 3955 cbvopab1g 5223 cbvmptfg 5257 cbviota 6524 sb8iota 6526 cbvriota 7400 2sb5nd 44557 |
Copyright terms: Public domain | W3C validator |