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 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 } ) )