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 ( ( 𝐹 = { ⟨ 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 } )