ex-cnv

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

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

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

Metamath Proof Explorer