# 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 ${⊢}\left({F}=\left\{⟨2,6⟩,⟨3,9⟩\right\}\wedge {B}=\left\{1,2\right\}\right)\to {F}\left[{B}\right]=\left\{6\right\}$

### Proof

Step Hyp Ref Expression
1 df-ima ${⊢}{F}\left[{B}\right]=\mathrm{ran}\left({{F}↾}_{{B}}\right)$
2 ex-res ${⊢}\left({F}=\left\{⟨2,6⟩,⟨3,9⟩\right\}\wedge {B}=\left\{1,2\right\}\right)\to {{F}↾}_{{B}}=\left\{⟨2,6⟩\right\}$
3 2 rneqd ${⊢}\left({F}=\left\{⟨2,6⟩,⟨3,9⟩\right\}\wedge {B}=\left\{1,2\right\}\right)\to \mathrm{ran}\left({{F}↾}_{{B}}\right)=\mathrm{ran}\left\{⟨2,6⟩\right\}$
4 1 3 syl5eq ${⊢}\left({F}=\left\{⟨2,6⟩,⟨3,9⟩\right\}\wedge {B}=\left\{1,2\right\}\right)\to {F}\left[{B}\right]=\mathrm{ran}\left\{⟨2,6⟩\right\}$
5 2ex ${⊢}2\in \mathrm{V}$
6 5 rnsnop ${⊢}\mathrm{ran}\left\{⟨2,6⟩\right\}=\left\{6\right\}$
7 4 6 eqtrdi ${⊢}\left({F}=\left\{⟨2,6⟩,⟨3,9⟩\right\}\wedge {B}=\left\{1,2\right\}\right)\to {F}\left[{B}\right]=\left\{6\right\}$