Description: Inverse point images under functions expressed as abstractions. (Contributed by Stefan O'Rear, 1-Feb-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | fniniseg2 | |- ( F Fn A -> ( `' F " { B } ) = { x e. A | ( F ` x ) = B } ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fncnvima2 | |- ( F Fn A -> ( `' F " { B } ) = { x e. A | ( F ` x ) e. { B } } ) |
|
2 | fvex | |- ( F ` x ) e. _V |
|
3 | 2 | elsn | |- ( ( F ` x ) e. { B } <-> ( F ` x ) = B ) |
4 | 3 | rabbii | |- { x e. A | ( F ` x ) e. { B } } = { x e. A | ( F ` x ) = B } |
5 | 1 4 | eqtrdi | |- ( F Fn A -> ( `' F " { B } ) = { x e. A | ( F ` x ) = B } ) |