Metamath Proof Explorer


Theorem opswap

Description: Swap the members of an ordered pair. (Contributed by NM, 14-Dec-2008) (Revised by Mario Carneiro, 30-Aug-2015)

Ref Expression
Assertion opswap { ⟨ 𝐴 , 𝐵 ⟩ } = ⟨ 𝐵 , 𝐴

Proof

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 { ⟨ 𝐴 , 𝐵 ⟩ } = ⟨ 𝐵 , 𝐴