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 F -> ( F ` A ) = U. ( F " { A } ) )

Proof

Step Hyp Ref Expression
1 fvex
 |-  ( F ` A ) e. _V
2 1 unisn
 |-  U. { ( F ` A ) } = ( F ` A )
3 eqid
 |-  dom F = dom F
4 df-fn
 |-  ( F Fn dom F <-> ( Fun F /\ dom F = dom F ) )
5 3 4 mpbiran2
 |-  ( F Fn dom F <-> Fun F )
6 fnsnfv
 |-  ( ( F Fn dom F /\ A e. dom F ) -> { ( F ` A ) } = ( F " { A } ) )
7 5 6 sylanbr
 |-  ( ( Fun F /\ A e. dom F ) -> { ( F ` A ) } = ( F " { A } ) )
8 7 unieqd
 |-  ( ( Fun F /\ A e. dom F ) -> U. { ( F ` A ) } = U. ( F " { A } ) )
9 2 8 eqtr3id
 |-  ( ( Fun F /\ A e. dom F ) -> ( F ` A ) = U. ( F " { A } ) )
10 9 ex
 |-  ( Fun F -> ( A e. dom F -> ( F ` A ) = U. ( F " { A } ) ) )
11 ndmfv
 |-  ( -. A e. dom F -> ( F ` A ) = (/) )
12 ndmima
 |-  ( -. A e. dom F -> ( F " { A } ) = (/) )
13 12 unieqd
 |-  ( -. A e. dom F -> U. ( F " { A } ) = U. (/) )
14 uni0
 |-  U. (/) = (/)
15 13 14 eqtrdi
 |-  ( -. A e. dom F -> U. ( F " { A } ) = (/) )
16 11 15 eqtr4d
 |-  ( -. A e. dom F -> ( F ` A ) = U. ( F " { A } ) )
17 10 16 pm2.61d1
 |-  ( Fun F -> ( F ` A ) = U. ( F " { A } ) )