Theorem afvelima

Description: Function value in an image, analogous to fvelima . (Contributed by Alexander van der Vekens, 25-May-2017)

	Ref	Expression
Assertion	afvelima	$$⊢\left(\mathrm{Fun}F\wedge A\in F\left[B\right]\right)\to \exists x\in B\left(F\mathrm{\text{'}\text{'}\text{'}}x\right)=A$$

Proof

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