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 BF\left(x\right)=A$$

Proof

Step	Hyp	Ref	Expression
1		funbrfv	$$⊢\mathrm{Fun}F\to \left(xFA\to F\left(x\right)=A\right)$$
2	1	reximdv	$$⊢\mathrm{Fun}F\to \left(\exists x\in BxFA\to \exists x\in BF\left(x\right)=A\right)$$
3		elimag	$$⊢A\in F\left[B\right]\to \left(A\in F\left[B\right]\leftrightarrow \exists x\in BxFA\right)$$
4	3	ibi	$$⊢A\in F\left[B\right]\to \exists x\in BxFA$$
5	2 4	impel	$$⊢\left(\mathrm{Fun}F\wedge A\in F\left[B\right]\right)\to \exists x\in BF\left(x\right)=A$$