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

Metamath Proof Explorer

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 eqtr3id ⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹 ) → ( 𝐹 ‘ 𝐴 ) = ∪ ( 𝐹 “ { 𝐴 } ) )
10 9 ex ⊢ ( Fun 𝐹 → ( 𝐴 ∈ dom 𝐹 → ( 𝐹 ‘ 𝐴 ) = ∪ ( 𝐹 “ { 𝐴 } ) ) )
11 ndmfv ⊢ ( ¬ 𝐴 ∈ dom 𝐹 → ( 𝐹 ‘ 𝐴 ) = ∅ )
12 ndmima ⊢ ( ¬ 𝐴 ∈ dom 𝐹 → ( 𝐹 “ { 𝐴 } ) = ∅ )
13 12 unieqd ⊢ ( ¬ 𝐴 ∈ dom 𝐹 → ∪ ( 𝐹 “ { 𝐴 } ) = ∪ ∅ )
14 uni0 ⊢ ∪ ∅ = ∅
15 13 14 eqtrdi ⊢ ( ¬ 𝐴 ∈ dom 𝐹 → ∪ ( 𝐹 “ { 𝐴 } ) = ∅ )
16 11 15 eqtr4d ⊢ ( ¬ 𝐴 ∈ dom 𝐹 → ( 𝐹 ‘ 𝐴 ) = ∪ ( 𝐹 “ { 𝐴 } ) )
17 10 16 pm2.61d1 ⊢ ( Fun 𝐹 → ( 𝐹 ‘ 𝐴 ) = ∪ ( 𝐹 “ { 𝐴 } ) )