Theorem funfv

Description: A simplified expression for the value of a function when we know it is a function. (Contributed by NM, 22-May-1998)

	Ref	Expression
Assertion	funfv	⊢ ( Fun 𝐹 → ( 𝐹 ‘ 𝐴 ) = ∪ ( 𝐹 “ { 𝐴 } ) )

Proof

Step	Hyp	Ref	Expression
1		fvex	⊢ ( 𝐹 ‘ 𝐴 ) ∈ V
2	1	unisn	⊢ ∪ { ( 𝐹 ‘ 𝐴 ) } = ( 𝐹 ‘ 𝐴 )
3		eqid	⊢ dom 𝐹 = dom 𝐹
4		df-fn	⊢ ( 𝐹 Fn dom 𝐹 ↔ ( Fun 𝐹 ∧ dom 𝐹 = dom 𝐹 ) )
5	3 4	mpbiran2	⊢ ( 𝐹 Fn dom 𝐹 ↔ Fun 𝐹 )
6		fnsnfv	⊢ ( ( 𝐹 Fn dom 𝐹 ∧ 𝐴 ∈ dom 𝐹 ) → { ( 𝐹 ‘ 𝐴 ) } = ( 𝐹 “ { 𝐴 } ) )
7	5 6	sylanbr	⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹 ) → { ( 𝐹 ‘ 𝐴 ) } = ( 𝐹 “ { 𝐴 } ) )
8	7	unieqd	⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹 ) → ∪ { ( 𝐹 ‘ 𝐴 ) } = ∪ ( 𝐹 “ { 𝐴 } ) )
9	2 8	syl5eqr	⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹 ) → ( 𝐹 ‘ 𝐴 ) = ∪ ( 𝐹 “ { 𝐴 } ) )
10	9	ex	⊢ ( Fun 𝐹 → ( 𝐴 ∈ dom 𝐹 → ( 𝐹 ‘ 𝐴 ) = ∪ ( 𝐹 “ { 𝐴 } ) ) )
11		ndmfv	⊢ ( ¬ 𝐴 ∈ dom 𝐹 → ( 𝐹 ‘ 𝐴 ) = ∅ )
12		ndmima	⊢ ( ¬ 𝐴 ∈ dom 𝐹 → ( 𝐹 “ { 𝐴 } ) = ∅ )
13	12	unieqd	⊢ ( ¬ 𝐴 ∈ dom 𝐹 → ∪ ( 𝐹 “ { 𝐴 } ) = ∪ ∅ )
14		uni0	⊢ ∪ ∅ = ∅
15	13 14	syl6eq	⊢ ( ¬ 𝐴 ∈ dom 𝐹 → ∪ ( 𝐹 “ { 𝐴 } ) = ∅ )
16	11 15	eqtr4d	⊢ ( ¬ 𝐴 ∈ dom 𝐹 → ( 𝐹 ‘ 𝐴 ) = ∪ ( 𝐹 “ { 𝐴 } ) )
17	10 16	pm2.61d1	⊢ ( Fun 𝐹 → ( 𝐹 ‘ 𝐴 ) = ∪ ( 𝐹 “ { 𝐴 } ) )