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 ⟩ } |