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	⊢ ( ( 𝐹 = { ⟨ 2 , 6 ⟩ , ⟨ 3 , 9 ⟩ } ∧ 𝐵 = { 1 , 2 } ) → ( 𝐹 “ 𝐵 ) = { 6 } )

Proof

Step	Hyp	Ref	Expression
1		df-ima	⊢ ( 𝐹 “ 𝐵 ) = ran ( 𝐹 ↾ 𝐵 )
2		ex-res	⊢ ( ( 𝐹 = { ⟨ 2 , 6 ⟩ , ⟨ 3 , 9 ⟩ } ∧ 𝐵 = { 1 , 2 } ) → ( 𝐹 ↾ 𝐵 ) = { ⟨ 2 , 6 ⟩ } )
3	2	rneqd	⊢ ( ( 𝐹 = { ⟨ 2 , 6 ⟩ , ⟨ 3 , 9 ⟩ } ∧ 𝐵 = { 1 , 2 } ) → ran ( 𝐹 ↾ 𝐵 ) = ran { ⟨ 2 , 6 ⟩ } )
4	1 3	syl5eq	⊢ ( ( 𝐹 = { ⟨ 2 , 6 ⟩ , ⟨ 3 , 9 ⟩ } ∧ 𝐵 = { 1 , 2 } ) → ( 𝐹 “ 𝐵 ) = ran { ⟨ 2 , 6 ⟩ } )
5		2ex	⊢ 2 ∈ V
6	5	rnsnop	⊢ ran { ⟨ 2 , 6 ⟩ } = { 6 }
7	4 6	eqtrdi	⊢ ( ( 𝐹 = { ⟨ 2 , 6 ⟩ , ⟨ 3 , 9 ⟩ } ∧ 𝐵 = { 1 , 2 } ) → ( 𝐹 “ 𝐵 ) = { 6 } )