Description: The predicate "is a filter." (Contributed by FL, 20-Jul-2007) (Revised by Mario Carneiro, 28-Jul-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | isfil | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-fil | |
|
2 | pweq | |
|
3 | 2 | adantr | |
4 | ineq1 | |
|
5 | 4 | neeq1d | |
6 | eleq2 | |
|
7 | 5 6 | imbi12d | |
8 | 7 | adantl | |
9 | 3 8 | raleqbidv | |
10 | fveq2 | |
|
11 | fvex | |
|
12 | elfvdm | |
|
13 | 1 9 10 11 12 | elmptrab2 | |