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