![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > filfbas | Structured version Visualization version Unicode version |
Description: A filter is a filter base. (Contributed by Jeff Hankins, 2-Sep-2009.) (Revised by Mario Carneiro, 28-Jul-2015.) |
Ref | Expression |
---|---|
filfbas |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | isfil 20910 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | simplbi 466 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1679 ax-4 1692 ax-5 1768 ax-6 1815 ax-7 1861 ax-8 1899 ax-9 1906 ax-10 1925 ax-11 1930 ax-12 1943 ax-13 2101 ax-ext 2441 ax-sep 4538 ax-nul 4547 ax-pow 4594 ax-pr 4652 |
This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-3an 993 df-tru 1457 df-ex 1674 df-nf 1678 df-sb 1808 df-eu 2313 df-mo 2314 df-clab 2448 df-cleq 2454 df-clel 2457 df-nfc 2591 df-ne 2634 df-ral 2753 df-rex 2754 df-rab 2757 df-v 3058 df-sbc 3279 df-csb 3375 df-dif 3418 df-un 3420 df-in 3422 df-ss 3429 df-nul 3743 df-if 3893 df-pw 3964 df-sn 3980 df-pr 3982 df-op 3986 df-uni 4212 df-br 4416 df-opab 4475 df-mpt 4476 df-id 4767 df-xp 4858 df-rel 4859 df-cnv 4860 df-co 4861 df-dm 4862 df-rn 4863 df-res 4864 df-ima 4865 df-iota 5564 df-fun 5602 df-fv 5608 df-fil 20909 |
This theorem is referenced by: 0nelfil 20912 filsspw 20914 filelss 20915 filin 20917 filtop 20918 snfbas 20929 fgfil 20938 elfilss 20939 filfinnfr 20940 fgabs 20942 filcon 20946 fgtr 20953 trfg 20954 ufilb 20969 ufilmax 20970 isufil2 20971 ssufl 20981 ufileu 20982 filufint 20983 ufilen 20993 fmfg 21012 fmufil 21022 fmid 21023 fmco 21024 ufldom 21025 hausflim 21044 flimrest 21046 flimclslem 21047 flfnei 21054 isflf 21056 flfcnp 21067 fclsrest 21087 fclsfnflim 21090 flimfnfcls 21091 isfcf 21097 cnpfcfi 21103 cnpfcf 21104 cnextcn 21130 cfilufg 21356 neipcfilu 21359 cnextucn 21366 ucnextcn 21367 cfilresi 22313 cfilres 22314 cmetss 22332 relcmpcmet 22334 cfilucfil3 22336 minveclem4a 22420 minveclem4aOLD 22432 filnetlem4 31085 |
Copyright terms: Public domain | W3C validator |