![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > filfbas | 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 17840 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | simplbi 447 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem is referenced by: 0nelfil 17842 filsspw 17844 filelss 17845 filin 17847 filtop 17848 snfbas 17859 fgfil 17868 elfilss 17869 filfinnfr 17870 fgabs 17872 filcon 17876 fgtr 17883 trfg 17884 ufilb 17899 ufilmax 17900 isufil2 17901 ssufl 17911 ufileu 17912 filufint 17913 ufilen 17923 fmfg 17942 fmufil 17952 fmid 17953 fmco 17954 ufldom 17955 hausflim 17974 flimrest 17976 flimclslem 17977 flfnei 17984 isflf 17986 flfcnp 17997 fclsrest 18017 fclsfnflim 18020 flimfnfcls 18021 isfcf 18027 cnpfcfi 18033 cnpfcf 18034 cnextcn 18059 cfilufg 18284 neipcfilu 18287 cnextucn 18294 ucnextcn 18295 cfilresi 19209 cfilres 19210 cmetss 19228 relcmpcmet 19230 cfilucfil3OLD 19232 cfilucfil3 19233 minveclem4a 19292 filnetlem4 26308 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1552 ax-5 1563 ax-17 1623 ax-9 1662 ax-8 1683 ax-13 1723 ax-14 1725 ax-6 1740 ax-7 1745 ax-11 1757 ax-12 1946 ax-ext 2393 ax-sep 4298 ax-nul 4306 ax-pow 4345 ax-pr 4371 |
This theorem depends on definitions: df-bi 178 df-or 360 df-an 361 df-3an 938 df-tru 1325 df-ex 1548 df-nf 1551 df-sb 1656 df-eu 2266 df-mo 2267 df-clab 2399 df-cleq 2405 df-clel 2408 df-nfc 2537 df-ne 2577 df-ral 2679 df-rex 2680 df-rab 2683 df-v 2926 df-sbc 3130 df-csb 3220 df-dif 3291 df-un 3293 df-in 3295 df-ss 3302 df-nul 3597 df-if 3708 df-pw 3769 df-sn 3788 df-pr 3789 df-op 3791 df-uni 3984 df-br 4181 df-opab 4235 df-mpt 4236 df-id 4466 df-xp 4851 df-rel 4852 df-cnv 4853 df-co 4854 df-dm 4855 df-rn 4856 df-res 4857 df-ima 4858 df-iota 5385 df-fun 5423 df-fv 5429 df-fil 17839 |
Copyright terms: Public domain | W3C validator |