Metamath Proof Explorer

Theorem fnimapr

Description: The image of a pair under a function. (Contributed by Jeff Madsen, 6-Jan-2011)

Ref Expression
Assertion fnimapr 
|- ( ( F Fn A /\ B e. A /\ C e. A ) -> ( F " { B , C } ) = { ( F ` B ) , ( F ` C ) } )

Proof

Step Hyp Ref Expression
1 fnsnfv 
 |-  ( ( F Fn A /\ B e. A ) -> { ( F ` B ) } = ( F " { B } ) )
2 1 3adant3 
 |-  ( ( F Fn A /\ B e. A /\ C e. A ) -> { ( F ` B ) } = ( F " { B } ) )
3 fnsnfv 
 |-  ( ( F Fn A /\ C e. A ) -> { ( F ` C ) } = ( F " { C } ) )
4 3 3adant2 
 |-  ( ( F Fn A /\ B e. A /\ C e. A ) -> { ( F ` C ) } = ( F " { C } ) )
5 2 4 uneq12d 
 |-  ( ( F Fn A /\ B e. A /\ C e. A ) -> ( { ( F ` B ) } u. { ( F ` C ) } ) = ( ( F " { B } ) u. ( F " { C } ) ) )
6 5 eqcomd 
 |-  ( ( F Fn A /\ B e. A /\ C e. A ) -> ( ( F " { B } ) u. ( F " { C } ) ) = ( { ( F ` B ) } u. { ( F ` C ) } ) )
7 df-pr 
 |-  { B , C } = ( { B } u. { C } )
8 7 imaeq2i 
 |-  ( F " { B , C } ) = ( F " ( { B } u. { C } ) )
9 imaundi 
 |-  ( F " ( { B } u. { C } ) ) = ( ( F " { B } ) u. ( F " { C } ) )
10 8 9 eqtri 
 |-  ( F " { B , C } ) = ( ( F " { B } ) u. ( F " { C } ) )
11 df-pr 
 |-  { ( F ` B ) , ( F ` C ) } = ( { ( F ` B ) } u. { ( F ` C ) } )
12 6 10 11 3eqtr4g 
 |-  ( ( F Fn A /\ B e. A /\ C e. A ) -> ( F " { B , C } ) = { ( F ` B ) , ( F ` C ) } )