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	⊢ ◡ { ⟨ 2 , 6 ⟩ , ⟨ 3 , 9 ⟩ } = { ⟨ 6 , 2 ⟩ , ⟨ 9 , 3 ⟩ }

Proof

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