# Metamath Proof Explorer

## Theorem fvelima

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 ${⊢}\left(\mathrm{Fun}{F}\wedge {A}\in {F}\left[{B}\right]\right)\to \exists {x}\in {B}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)={A}$

### Proof

Step Hyp Ref Expression
1 funbrfv ${⊢}\mathrm{Fun}{F}\to \left({x}{F}{A}\to {F}\left({x}\right)={A}\right)$
2 1 reximdv ${⊢}\mathrm{Fun}{F}\to \left(\exists {x}\in {B}\phantom{\rule{.4em}{0ex}}{x}{F}{A}\to \exists {x}\in {B}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)={A}\right)$
3 elimag ${⊢}{A}\in {F}\left[{B}\right]\to \left({A}\in {F}\left[{B}\right]↔\exists {x}\in {B}\phantom{\rule{.4em}{0ex}}{x}{F}{A}\right)$
4 3 ibi ${⊢}{A}\in {F}\left[{B}\right]\to \exists {x}\in {B}\phantom{\rule{.4em}{0ex}}{x}{F}{A}$
5 2 4 impel ${⊢}\left(\mathrm{Fun}{F}\wedge {A}\in {F}\left[{B}\right]\right)\to \exists {x}\in {B}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)={A}$