This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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	$⊢ (Fun F \land A \in F [B]) \to \exists x \in B F (x) = A$

Proof

Step	Hyp	Ref	Expression
1		funbrfv	$⊢ Fun F \to (x F A \to F (x) = A)$
2	1	reximdv	$⊢ Fun F \to (\exists x \in B x F A \to \exists x \in B F (x) = A)$
3		elimag	$⊢ A \in F [B] \to (A \in F [B] \leftrightarrow \exists x \in B x F A)$
4	3	ibi	$⊢ A \in F [B] \to \exists x \in B x F A$
5	2 4	impel	$⊢ (Fun F \land A \in F [B]) \to \exists x \in B F (x) = A$