![]() |
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 2322 for a version with an additional disjoint variable condition on 𝑥, 𝑧 but not requiring ax-13 2370. (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 2370. Use nfsbv 2322 instead. (New usage is discouraged.) |
Ref | Expression |
---|---|
nfsb.1 | ⊢ Ⅎ𝑧𝜑 |
Ref | Expression |
---|---|
nfsb | ⊢ Ⅎ𝑧[𝑦 / 𝑥]𝜑 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nftru 1805 | . . 3 ⊢ Ⅎ𝑥⊤ | |
2 | nfsb.1 | . . . 4 ⊢ Ⅎ𝑧𝜑 | |
3 | 2 | a1i 11 | . . 3 ⊢ (⊤ → Ⅎ𝑧𝜑) |
4 | 1, 3 | nfsbd 2520 | . 2 ⊢ (⊤ → Ⅎ𝑧[𝑦 / 𝑥]𝜑) |
5 | 4 | mptru 1547 | 1 ⊢ Ⅎ𝑧[𝑦 / 𝑥]𝜑 |
Colors of variables: wff setvar class |
Syntax hints: ⊤wtru 1541 Ⅎwnf 1784 [wsb 2066 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-10 2136 ax-11 2153 ax-12 2170 ax-13 2370 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-tru 1543 df-ex 1781 df-nf 1785 df-sb 2067 |
This theorem is referenced by: hbsb 2522 sb10f 2525 2sb8e 2528 sb8eu 2593 cbvralf 3355 cbvralsv 3361 cbvrexsv 3362 cbvreu 3423 cbvrab 3472 cbvreucsf 3940 cbvrabcsf 3941 cbvopab1g 5224 cbvmptfg 5258 cbviota 6505 sb8iota 6507 cbvriota 7382 2sb5nd 43624 |
Copyright terms: Public domain | W3C validator |