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

Definition df-fbas 16704
 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 16694 . 2
2 vw . . 3
3 cvv 2958 . . 3
4 vx . . . . . . 7
54cv 1652 . . . . . 6
6 c0 3630 . . . . . 6
75, 6wne 2601 . . . . 5
86, 5wnel 2602 . . . . 5
9 vy . . . . . . . . . . . 12
109cv 1652 . . . . . . . . . . 11
11 vz . . . . . . . . . . . 12
1211cv 1652 . . . . . . . . . . 11
1310, 12cin 3321 . . . . . . . . . 10
1413cpw 3801 . . . . . . . . 9
155, 14cin 3321 . . . . . . . 8
1615, 6wne 2601 . . . . . . 7
1716, 11, 5wral 2707 . . . . . 6
1817, 9, 5wral 2707 . . . . 5
197, 8, 18w3a 937 . . . 4
202cv 1652 . . . . . 6
2120cpw 3801 . . . . 5
2221cpw 3801 . . . 4
2319, 4, 22crab 2711 . . 3
242, 3, 23cmpt 4269 . 2
251, 24wceq 1653 1
 Colors of variables: wff set class This definition is referenced by:  isfbas  17866
 Copyright terms: Public domain W3C validator