![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > nfs1v | GIF version |
Description: 𝑥 is not free in [𝑦 / 𝑥]𝜑 when 𝑥 and 𝑦 are distinct. (Contributed by Mario Carneiro, 11-Aug-2016.) |
Ref | Expression |
---|---|
nfs1v | ⊢ Ⅎ𝑥[𝑦 / 𝑥]𝜑 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hbs1 1869 | . 2 ⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑) | |
2 | 1 | nfi 1403 | 1 ⊢ Ⅎ𝑥[𝑦 / 𝑥]𝜑 |
Colors of variables: wff set class |
Syntax hints: Ⅎwnf 1401 [wsb 1699 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1388 ax-gen 1390 ax-ie1 1434 ax-ie2 1435 ax-8 1447 ax-11 1449 ax-4 1452 ax-17 1471 ax-i9 1475 ax-ial 1479 |
This theorem depends on definitions: df-bi 116 df-nf 1402 df-sb 1700 |
This theorem is referenced by: nfsbxy 1873 nfsbxyt 1874 sbco3v 1898 sbcomxyyz 1901 sbnf2 1912 mo2n 1983 mo23 1996 mor 1997 clelab 2219 cbvralf 2598 cbvrexf 2599 cbvralsv 2615 cbvrexsv 2616 cbvrab 2631 sbhypf 2682 mob2 2809 reu2 2817 sbcralt 2929 sbcrext 2930 sbcralg 2931 sbcreug 2933 sbcel12g 2960 sbceqg 2961 cbvreucsf 3006 cbvrabcsf 3007 disjiun 3862 cbvopab1 3933 cbvopab1s 3935 csbopabg 3938 cbvmptf 3954 cbvmpt 3955 opelopabsb 4111 frind 4203 tfis 4426 findes 4446 opeliunxp 4522 ralxpf 4613 rexxpf 4614 cbviota 5019 csbiotag 5042 isarep1 5134 cbvriota 5656 csbriotag 5658 abrexex2g 5929 abrexex2 5933 dfoprab4f 6001 finexdc 6698 ssfirab 6723 uzind4s 9177 zsupcllemstep 11368 bezoutlemmain 11414 cbvrald 12405 bj-bdfindes 12561 bj-findes 12593 |
Copyright terms: Public domain | W3C validator |