This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ◡ { ⟨ 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 ⟩ }