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 𝐹 → ( 𝐹𝐴 ) = ( 𝐹 “ { 𝐴 } ) )