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