| 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 2330 for a version with an additional disjoint variable condition on 𝑥, 𝑧 but not requiring ax-13 2377. (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 2377. Use nfsbv 2330 instead. (New usage is discouraged.) |
| Ref | Expression |
|---|---|
| nfsb.1 | ⊢ Ⅎ𝑧𝜑 |
| Ref | Expression |
|---|---|
| nfsb | ⊢ Ⅎ𝑧[𝑦 / 𝑥]𝜑 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nftru 1804 | . . 3 ⊢ Ⅎ𝑥⊤ | |
| 2 | nfsb.1 | . . . 4 ⊢ Ⅎ𝑧𝜑 | |
| 3 | 2 | a1i 11 | . . 3 ⊢ (⊤ → Ⅎ𝑧𝜑) |
| 4 | 1, 3 | nfsbd 2527 | . 2 ⊢ (⊤ → Ⅎ𝑧[𝑦 / 𝑥]𝜑) |
| 5 | 4 | mptru 1547 | 1 ⊢ Ⅎ𝑧[𝑦 / 𝑥]𝜑 |
| Colors of variables: wff setvar class |
| Syntax hints: ⊤wtru 1541 Ⅎwnf 1783 [wsb 2064 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-10 2141 ax-11 2157 ax-12 2177 ax-13 2377 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-tru 1543 df-ex 1780 df-nf 1784 df-sb 2065 |
| This theorem is referenced by: hbsb 2529 sb10f 2532 2sb8e 2535 sb8eu 2600 cbvralf 3360 cbvralsv 3366 cbvrexsv 3367 cbvreu 3428 cbvrab 3479 cbvreucsf 3943 cbvrabcsf 3944 cbvopab1g 5218 cbvmptfg 5252 cbviota 6523 sb8iota 6525 cbvriota 7401 2sb5nd 44580 |
| Copyright terms: Public domain | W3C validator |