Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-fbas Unicode version

Definition df-fbas 16654
 Description: Define the class of all filter bases. Note that a filter base on one set is also a filter base for any superset, so there is not a unique base set that can be recovered. (Contributed by Jeff Hankins, 1-Sep-2009.) (Revised by Stefan O'Rear, 11-Jul-2015.)
Assertion
Ref Expression
df-fbas
Distinct variable group:   ,,,

Detailed syntax breakdown of Definition df-fbas
StepHypRef Expression
1 cfbas 16644 . 2
2 vw . . 3
3 cvv 2916 . . 3
4 vx . . . . . . 7
54cv 1648 . . . . . 6
6 c0 3588 . . . . . 6
75, 6wne 2567 . . . . 5
86, 5wnel 2568 . . . . 5
9 vy . . . . . . . . . . . 12
109cv 1648 . . . . . . . . . . 11
11 vz . . . . . . . . . . . 12
1211cv 1648 . . . . . . . . . . 11
1310, 12cin 3279 . . . . . . . . . 10
1413cpw 3759 . . . . . . . . 9
155, 14cin 3279 . . . . . . . 8
1615, 6wne 2567 . . . . . . 7
1716, 11, 5wral 2666 . . . . . 6
1817, 9, 5wral 2666 . . . . 5
197, 8, 18w3a 936 . . . 4
202cv 1648 . . . . . 6
2120cpw 3759 . . . . 5
2221cpw 3759 . . . 4
2319, 4, 22crab 2670 . . 3
242, 3, 23cmpt 4226 . 2
251, 24wceq 1649 1
 Colors of variables: wff set class This definition is referenced by:  isfbas  17814
 Copyright terms: Public domain W3C validator