# Metamath Proof Explorer

## Theorem ex-rn

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

Ref Expression
Assertion ex-rn ${⊢}{F}=\left\{⟨2,6⟩,⟨3,9⟩\right\}\to \mathrm{ran}{F}=\left\{6,9\right\}$

### Proof

Step Hyp Ref Expression
1 rneq ${⊢}{F}=\left\{⟨2,6⟩,⟨3,9⟩\right\}\to \mathrm{ran}{F}=\mathrm{ran}\left\{⟨2,6⟩,⟨3,9⟩\right\}$
2 df-pr ${⊢}\left\{⟨2,6⟩,⟨3,9⟩\right\}=\left\{⟨2,6⟩\right\}\cup \left\{⟨3,9⟩\right\}$
3 2 rneqi ${⊢}\mathrm{ran}\left\{⟨2,6⟩,⟨3,9⟩\right\}=\mathrm{ran}\left(\left\{⟨2,6⟩\right\}\cup \left\{⟨3,9⟩\right\}\right)$
4 rnun ${⊢}\mathrm{ran}\left(\left\{⟨2,6⟩\right\}\cup \left\{⟨3,9⟩\right\}\right)=\mathrm{ran}\left\{⟨2,6⟩\right\}\cup \mathrm{ran}\left\{⟨3,9⟩\right\}$
5 2nn ${⊢}2\in ℕ$
6 5 elexi ${⊢}2\in \mathrm{V}$
7 6 rnsnop ${⊢}\mathrm{ran}\left\{⟨2,6⟩\right\}=\left\{6\right\}$
8 3nn ${⊢}3\in ℕ$
9 8 elexi ${⊢}3\in \mathrm{V}$
10 9 rnsnop ${⊢}\mathrm{ran}\left\{⟨3,9⟩\right\}=\left\{9\right\}$
11 7 10 uneq12i ${⊢}\mathrm{ran}\left\{⟨2,6⟩\right\}\cup \mathrm{ran}\left\{⟨3,9⟩\right\}=\left\{6\right\}\cup \left\{9\right\}$
12 df-pr ${⊢}\left\{6,9\right\}=\left\{6\right\}\cup \left\{9\right\}$
13 11 12 eqtr4i ${⊢}\mathrm{ran}\left\{⟨2,6⟩\right\}\cup \mathrm{ran}\left\{⟨3,9⟩\right\}=\left\{6,9\right\}$
14 3 4 13 3eqtri ${⊢}\mathrm{ran}\left\{⟨2,6⟩,⟨3,9⟩\right\}=\left\{6,9\right\}$
15 1 14 eqtrdi ${⊢}{F}=\left\{⟨2,6⟩,⟨3,9⟩\right\}\to \mathrm{ran}{F}=\left\{6,9\right\}$