Step |
Hyp |
Ref |
Expression |
1 |
|
fveq2 |
|- ( x = X -> ( Fil ` x ) = ( Fil ` X ) ) |
2 |
|
fveq2 |
|- ( x = X -> ( UFil ` x ) = ( UFil ` X ) ) |
3 |
2
|
rexeqdv |
|- ( x = X -> ( E. g e. ( UFil ` x ) f C_ g <-> E. g e. ( UFil ` X ) f C_ g ) ) |
4 |
1 3
|
raleqbidv |
|- ( x = X -> ( A. f e. ( Fil ` x ) E. g e. ( UFil ` x ) f C_ g <-> A. f e. ( Fil ` X ) E. g e. ( UFil ` X ) f C_ g ) ) |
5 |
|
df-ufl |
|- UFL = { x | A. f e. ( Fil ` x ) E. g e. ( UFil ` x ) f C_ g } |
6 |
4 5
|
elab2g |
|- ( X e. V -> ( X e. UFL <-> A. f e. ( Fil ` X ) E. g e. ( UFil ` X ) f C_ g ) ) |