Description: The property of being a locally A topological space. (Contributed by Mario Carneiro, 2-Mar-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | islly | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ineq1 | |
|
2 | oveq1 | |
|
3 | 2 | eleq1d | |
4 | 3 | anbi2d | |
5 | 1 4 | rexeqbidv | |
6 | 5 | ralbidv | |
7 | 6 | raleqbi1dv | |
8 | df-lly | |
|
9 | 7 8 | elrab2 | |