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 1814 | . 2 ⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑) | |
2 | 1 | nfi 1351 | 1 ⊢ Ⅎ𝑥[𝑦 / 𝑥]𝜑 |
Colors of variables: wff set class |
Syntax hints: Ⅎwnf 1349 [wsb 1645 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-5 1336 ax-gen 1338 ax-ie1 1382 ax-ie2 1383 ax-8 1395 ax-11 1397 ax-4 1400 ax-17 1419 ax-i9 1423 ax-ial 1427 |
This theorem depends on definitions: df-bi 110 df-nf 1350 df-sb 1646 |
This theorem is referenced by: nfsbxy 1818 nfsbxyt 1819 sbco3v 1843 sbcomxyyz 1846 sbnf2 1857 mo2n 1928 mo23 1941 mor 1942 clelab 2162 cbvralf 2527 cbvrexf 2528 cbvralsv 2544 cbvrexsv 2545 cbvrab 2555 sbhypf 2603 mob2 2721 reu2 2729 sbcralt 2834 sbcrext 2835 sbcralg 2836 sbcreug 2838 sbcel12g 2865 sbceqg 2866 cbvreucsf 2910 cbvrabcsf 2911 cbvopab1 3830 cbvopab1s 3832 csbopabg 3835 cbvmpt 3851 opelopabsb 3997 frind 4089 tfis 4306 findes 4326 opeliunxp 4395 ralxpf 4482 rexxpf 4483 cbviota 4872 csbiotag 4895 isarep1 4985 cbvriota 5478 csbriotag 5480 abrexex2g 5747 abrexex2 5751 dfoprab4f 5819 uzind4s 8533 cbvrald 9927 bj-bdfindes 10074 bj-findes 10106 |
Copyright terms: Public domain | W3C validator |