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

Metamath Proof Explorer

Theorem funfv2

Description: The value of a function. Definition of function value in Enderton p. 43. (Contributed by NM, 22-May-1998)

		Ref	Expression
	Assertion	funfv2	$⊢ Fun F \to F (A) = ⋃ \{y \| A F y\}$

Step	Hyp	Ref	Expression
1		funfv	$⊢ Fun F \to F (A) = ⋃ F [\{A\}]$
2		funrel	$⊢ Fun F \to Rel F$
3		relimasn	$⊢ Rel F \to F [\{A\}] = \{y \| A F y\}$
4	2 3	syl	$⊢ Fun F \to F [\{A\}] = \{y \| A F y\}$
5	4	unieqd	$⊢ Fun F \to ⋃ F [\{A\}] = ⋃ \{y \| A F y\}$
6	1 5	eqtrd	$⊢ Fun F \to F (A) = ⋃ \{y \| A F y\}$