# Metamath Proof Explorer

## Theorem ex-cnv

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

Ref Expression
Assertion ex-cnv ${⊢}{\left\{⟨2,6⟩,⟨3,9⟩\right\}}^{-1}=\left\{⟨6,2⟩,⟨9,3⟩\right\}$

### Proof

Step Hyp Ref Expression
1 cnvun ${⊢}{\left(\left\{⟨2,6⟩\right\}\cup \left\{⟨3,9⟩\right\}\right)}^{-1}={\left\{⟨2,6⟩\right\}}^{-1}\cup {\left\{⟨3,9⟩\right\}}^{-1}$
2 2nn ${⊢}2\in ℕ$
3 2 elexi ${⊢}2\in \mathrm{V}$
4 6nn ${⊢}6\in ℕ$
5 4 elexi ${⊢}6\in \mathrm{V}$
6 3 5 cnvsn ${⊢}{\left\{⟨2,6⟩\right\}}^{-1}=\left\{⟨6,2⟩\right\}$
7 3nn ${⊢}3\in ℕ$
8 7 elexi ${⊢}3\in \mathrm{V}$
9 9nn ${⊢}9\in ℕ$
10 9 elexi ${⊢}9\in \mathrm{V}$
11 8 10 cnvsn ${⊢}{\left\{⟨3,9⟩\right\}}^{-1}=\left\{⟨9,3⟩\right\}$
12 6 11 uneq12i ${⊢}{\left\{⟨2,6⟩\right\}}^{-1}\cup {\left\{⟨3,9⟩\right\}}^{-1}=\left\{⟨6,2⟩\right\}\cup \left\{⟨9,3⟩\right\}$
13 1 12 eqtri ${⊢}{\left(\left\{⟨2,6⟩\right\}\cup \left\{⟨3,9⟩\right\}\right)}^{-1}=\left\{⟨6,2⟩\right\}\cup \left\{⟨9,3⟩\right\}$
14 df-pr ${⊢}\left\{⟨2,6⟩,⟨3,9⟩\right\}=\left\{⟨2,6⟩\right\}\cup \left\{⟨3,9⟩\right\}$
15 14 cnveqi ${⊢}{\left\{⟨2,6⟩,⟨3,9⟩\right\}}^{-1}={\left(\left\{⟨2,6⟩\right\}\cup \left\{⟨3,9⟩\right\}\right)}^{-1}$
16 df-pr ${⊢}\left\{⟨6,2⟩,⟨9,3⟩\right\}=\left\{⟨6,2⟩\right\}\cup \left\{⟨9,3⟩\right\}$
17 13 15 16 3eqtr4i ${⊢}{\left\{⟨2,6⟩,⟨3,9⟩\right\}}^{-1}=\left\{⟨6,2⟩,⟨9,3⟩\right\}$