Metamath Proof Explorer

Theorem ex-ima

Description: Example for df-ima . Example by David A. Wheeler. (Contributed by Mario Carneiro, 7-May-2015)

Ref Expression
Assertion ex-ima 
|- ( ( F = { <. 2 , 6 >. , <. 3 , 9 >. } /\ B = { 1 , 2 } ) -> ( F " B ) = { 6 } )

Proof

Step Hyp Ref Expression
1 df-ima 
 |-  ( F " B ) = ran ( F |` B )
2 ex-res 
 |-  ( ( F = { <. 2 , 6 >. , <. 3 , 9 >. } /\ B = { 1 , 2 } ) -> ( F |` B ) = { <. 2 , 6 >. } )
3 2 rneqd 
 |-  ( ( F = { <. 2 , 6 >. , <. 3 , 9 >. } /\ B = { 1 , 2 } ) -> ran ( F |` B ) = ran { <. 2 , 6 >. } )
4 1 3 eqtrid 
 |-  ( ( F = { <. 2 , 6 >. , <. 3 , 9 >. } /\ B = { 1 , 2 } ) -> ( F " B ) = ran { <. 2 , 6 >. } )
5 2ex 
 |-  2 e. _V
6 5 rnsnop 
 |-  ran { <. 2 , 6 >. } = { 6 }
7 4 6 eqtrdi 
 |-  ( ( F = { <. 2 , 6 >. , <. 3 , 9 >. } /\ B = { 1 , 2 } ) -> ( F " B ) = { 6 } )