Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-fbas Unicode version

Definition df-fbas 12170
 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 12161 . 2
2 vw . . 3
3 cvv 2686 . . 3
4 vx . . . . . . 7
54cv 1330 . . . . . 6
6 c0 3363 . . . . . 6
75, 6wne 2308 . . . . 5
86, 5wnel 2403 . . . . 5
9 vy . . . . . . . . . . . 12
109cv 1330 . . . . . . . . . . 11
11 vz . . . . . . . . . . . 12
1211cv 1330 . . . . . . . . . . 11
1310, 12cin 3070 . . . . . . . . . 10
1413cpw 3510 . . . . . . . . 9
155, 14cin 3070 . . . . . . . 8
1615, 6wne 2308 . . . . . . 7
1716, 11, 5wral 2416 . . . . . 6
1817, 9, 5wral 2416 . . . . 5
197, 8, 18w3a 962 . . . 4
202cv 1330 . . . . . 6
2120cpw 3510 . . . . 5
2221cpw 3510 . . . 4
2319, 4, 22crab 2420 . . 3
242, 3, 23cmpt 3989 . 2
251, 24wceq 1331 1
 Colors of variables: wff set class This definition is referenced by: (None)
 Copyright terms: Public domain W3C validator