Description: Function value in an image. Part of Theorem 4.4(iii) of Monk1 p. 42. (Contributed by NM, 29-Apr-2004) (Proof shortened by Andrew Salmon, 22-Oct-2011)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | fvelima | |- ( ( Fun F /\ A e. ( F " B ) ) -> E. x e. B ( F ` x ) = A ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | funbrfv | |- ( Fun F -> ( x F A -> ( F ` x ) = A ) ) |
|
| 2 | 1 | reximdv | |- ( Fun F -> ( E. x e. B x F A -> E. x e. B ( F ` x ) = A ) ) |
| 3 | elimag | |- ( A e. ( F " B ) -> ( A e. ( F " B ) <-> E. x e. B x F A ) ) |
|
| 4 | 3 | ibi | |- ( A e. ( F " B ) -> E. x e. B x F A ) |
| 5 | 2 4 | impel | |- ( ( Fun F /\ A e. ( F " B ) ) -> E. x e. B ( F ` x ) = A ) |