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 𝐹 → ( 𝐹 ‘ 𝐴 ) = ∪ { 𝑦 ∣ 𝐴 𝐹 𝑦 } )

Proof

Step	Hyp	Ref	Expression
1		funfv	⊢ ( Fun 𝐹 → ( 𝐹 ‘ 𝐴 ) = ∪ ( 𝐹 “ { 𝐴 } ) )
2		funrel	⊢ ( Fun 𝐹 → Rel 𝐹 )
3		relimasn	⊢ ( Rel 𝐹 → ( 𝐹 “ { 𝐴 } ) = { 𝑦 ∣ 𝐴 𝐹 𝑦 } )
4	2 3	syl	⊢ ( Fun 𝐹 → ( 𝐹 “ { 𝐴 } ) = { 𝑦 ∣ 𝐴 𝐹 𝑦 } )
5	4	unieqd	⊢ ( Fun 𝐹 → ∪ ( 𝐹 “ { 𝐴 } ) = ∪ { 𝑦 ∣ 𝐴 𝐹 𝑦 } )
6	1 5	eqtrd	⊢ ( Fun 𝐹 → ( 𝐹 ‘ 𝐴 ) = ∪ { 𝑦 ∣ 𝐴 𝐹 𝑦 } )