![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > nfs1v | Unicode version |
Description: ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
nfs1v |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hbs1 1811 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | nfi 1348 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
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 1333 ax-gen 1335 ax-ie1 1379 ax-ie2 1380 ax-8 1392 ax-11 1394 ax-4 1397 ax-17 1416 ax-i9 1420 ax-ial 1424 |
This theorem depends on definitions: df-bi 110 df-nf 1347 df-sb 1643 |
This theorem is referenced by: nfsbxy 1815 nfsbxyt 1816 sbco3v 1840 sbcomxyyz 1843 sbnf2 1854 mo2n 1925 mo23 1938 mor 1939 clelab 2159 cbvralf 2521 cbvrexf 2522 cbvralsv 2538 cbvrexsv 2539 cbvrab 2549 sbhypf 2597 mob2 2715 reu2 2723 sbcralt 2828 sbcrext 2829 sbcralg 2830 sbcrexg 2831 sbcreug 2832 sbcel12g 2859 sbceqg 2860 cbvreucsf 2904 cbvrabcsf 2905 cbvopab1 3821 cbvopab1s 3823 csbopabg 3826 cbvmpt 3842 opelopabsb 3988 tfis 4249 findes 4269 opeliunxp 4338 ralxpf 4425 rexxpf 4426 cbviota 4815 csbiotag 4838 isarep1 4928 cbvriota 5421 csbriotag 5423 abrexex2g 5689 abrexex2 5693 dfoprab4f 5761 uzind4s 8309 cbvrald 9262 bj-bdfindes 9409 bj-findes 9441 |
Copyright terms: Public domain | W3C validator |