Step |
Hyp |
Ref |
Expression |
1 |
|
cnvsng |
⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ◡ { 〈 𝐴 , 𝐵 〉 } = { 〈 𝐵 , 𝐴 〉 } ) |
2 |
1
|
unieqd |
⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ∪ ◡ { 〈 𝐴 , 𝐵 〉 } = ∪ { 〈 𝐵 , 𝐴 〉 } ) |
3 |
|
opex |
⊢ 〈 𝐵 , 𝐴 〉 ∈ V |
4 |
3
|
unisn |
⊢ ∪ { 〈 𝐵 , 𝐴 〉 } = 〈 𝐵 , 𝐴 〉 |
5 |
2 4
|
eqtrdi |
⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ∪ ◡ { 〈 𝐴 , 𝐵 〉 } = 〈 𝐵 , 𝐴 〉 ) |
6 |
|
uni0 |
⊢ ∪ ∅ = ∅ |
7 |
|
opprc |
⊢ ( ¬ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → 〈 𝐴 , 𝐵 〉 = ∅ ) |
8 |
7
|
sneqd |
⊢ ( ¬ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → { 〈 𝐴 , 𝐵 〉 } = { ∅ } ) |
9 |
8
|
cnveqd |
⊢ ( ¬ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ◡ { 〈 𝐴 , 𝐵 〉 } = ◡ { ∅ } ) |
10 |
|
cnvsn0 |
⊢ ◡ { ∅ } = ∅ |
11 |
9 10
|
eqtrdi |
⊢ ( ¬ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ◡ { 〈 𝐴 , 𝐵 〉 } = ∅ ) |
12 |
11
|
unieqd |
⊢ ( ¬ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ∪ ◡ { 〈 𝐴 , 𝐵 〉 } = ∪ ∅ ) |
13 |
|
ancom |
⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ↔ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) |
14 |
|
opprc |
⊢ ( ¬ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) → 〈 𝐵 , 𝐴 〉 = ∅ ) |
15 |
13 14
|
sylnbi |
⊢ ( ¬ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → 〈 𝐵 , 𝐴 〉 = ∅ ) |
16 |
6 12 15
|
3eqtr4a |
⊢ ( ¬ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ∪ ◡ { 〈 𝐴 , 𝐵 〉 } = 〈 𝐵 , 𝐴 〉 ) |
17 |
5 16
|
pm2.61i |
⊢ ∪ ◡ { 〈 𝐴 , 𝐵 〉 } = 〈 𝐵 , 𝐴 〉 |