Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > nfs1v | Unicode 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 1891 | . 2 | |
2 | 1 | nfi 1423 | 1 |
Colors of variables: wff set class |
Syntax hints: wnf 1421 wsb 1720 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1408 ax-gen 1410 ax-ie1 1454 ax-ie2 1455 ax-8 1467 ax-11 1469 ax-4 1472 ax-17 1491 ax-i9 1495 ax-ial 1499 |
This theorem depends on definitions: df-bi 116 df-nf 1422 df-sb 1721 |
This theorem is referenced by: nfsbxy 1895 nfsbxyt 1896 sbco3v 1920 sbcomxyyz 1923 sbnf2 1934 mo2n 2005 mo23 2018 mor 2019 clelab 2242 cbvralf 2625 cbvrexf 2626 cbvralsv 2642 cbvrexsv 2643 cbvrab 2658 sbhypf 2709 mob2 2837 reu2 2845 sbcralt 2957 sbcrext 2958 sbcralg 2959 sbcreug 2961 sbcel12g 2988 sbceqg 2989 cbvreucsf 3034 cbvrabcsf 3035 disjiun 3894 cbvopab1 3971 cbvopab1s 3973 csbopabg 3976 cbvmptf 3992 cbvmpt 3993 opelopabsb 4152 frind 4244 tfis 4467 findes 4487 opeliunxp 4564 ralxpf 4655 rexxpf 4656 cbviota 5063 csbiotag 5086 isarep1 5179 cbvriota 5708 csbriotag 5710 abrexex2g 5986 abrexex2 5990 dfoprab4f 6059 finexdc 6764 ssfirab 6790 uzind4s 9353 zsupcllemstep 11565 bezoutlemmain 11613 cbvrald 12922 bj-bdfindes 13074 bj-findes 13106 |
Copyright terms: Public domain | W3C validator |