![]() |
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 𝜑, it is not free in [𝑦 / 𝑥]𝜑 when 𝑦 and 𝑧 are distinct. For a version requiring more disjoint variables, but fewer axioms, see nfsbv 2312. (Contributed by Mario Carneiro, 11-Aug-2016.) |
Ref | Expression |
---|---|
nfsb.1 | ⊢ Ⅎ𝑧𝜑 |
Ref | Expression |
---|---|
nfsb | ⊢ Ⅎ𝑧[𝑦 / 𝑥]𝜑 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | axc16nf 2227 | . 2 ⊢ (∀𝑧 𝑧 = 𝑦 → Ⅎ𝑧[𝑦 / 𝑥]𝜑) | |
2 | nfsb.1 | . . 3 ⊢ Ⅎ𝑧𝜑 | |
3 | 2 | nfsb4 2494 | . 2 ⊢ (¬ ∀𝑧 𝑧 = 𝑦 → Ⅎ𝑧[𝑦 / 𝑥]𝜑) |
4 | 1, 3 | pm2.61i 183 | 1 ⊢ Ⅎ𝑧[𝑦 / 𝑥]𝜑 |
Colors of variables: wff setvar class |
Syntax hints: ∀wal 1520 Ⅎwnf 1765 [wsb 2042 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-10 2112 ax-11 2126 ax-12 2141 ax-13 2344 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-tru 1525 df-ex 1762 df-nf 1766 df-sb 2043 |
This theorem is referenced by: hbsb 2519 sb10f 2524 2sb8e 2530 sb8eu 2652 cbvralf 3397 cbvreu 3401 cbvralsv 3415 cbvrexsv 3416 cbvrab 3433 cbvreucsf 3851 cbvrabcsf 3852 cbvopab1 5035 cbvmptf 5059 cbvmpt 5060 ralxpf 5603 cbviota 6194 sb8iota 6196 cbvriota 6987 dfoprab4f 7610 mo5f 29945 ax11-pm2 33729 2sb5nd 40433 dfich2 43095 dfich2ai 43096 dfich2OLD 43098 ichbi12i 43100 |
Copyright terms: Public domain | W3C validator |