Theorem 2nd1st

Description: Swap the members of an ordered pair. (Contributed by NM, 31-Dec-2014)

	Ref	Expression
Assertion	2nd1st	⊢ ( 𝐴 ∈ ( 𝐵 × 𝐶 ) → ∪ ◡ { 𝐴 } = ⟨ ( 2nd ‘ 𝐴 ) , ( 1st ‘ 𝐴 ) ⟩ )

Proof

Step	Hyp	Ref	Expression
1		1st2nd2	⊢ ( 𝐴 ∈ ( 𝐵 × 𝐶 ) → 𝐴 = ⟨ ( 1st ‘ 𝐴 ) , ( 2nd ‘ 𝐴 ) ⟩ )
2	1	sneqd	⊢ ( 𝐴 ∈ ( 𝐵 × 𝐶 ) → { 𝐴 } = { ⟨ ( 1st ‘ 𝐴 ) , ( 2nd ‘ 𝐴 ) ⟩ } )
3	2	cnveqd	⊢ ( 𝐴 ∈ ( 𝐵 × 𝐶 ) → ◡ { 𝐴 } = ◡ { ⟨ ( 1st ‘ 𝐴 ) , ( 2nd ‘ 𝐴 ) ⟩ } )
4	3	unieqd	⊢ ( 𝐴 ∈ ( 𝐵 × 𝐶 ) → ∪ ◡ { 𝐴 } = ∪ ◡ { ⟨ ( 1st ‘ 𝐴 ) , ( 2nd ‘ 𝐴 ) ⟩ } )
5		opswap	⊢ ∪ ◡ { ⟨ ( 1st ‘ 𝐴 ) , ( 2nd ‘ 𝐴 ) ⟩ } = ⟨ ( 2nd ‘ 𝐴 ) , ( 1st ‘ 𝐴 ) ⟩
6	4 5	eqtrdi	⊢ ( 𝐴 ∈ ( 𝐵 × 𝐶 ) → ∪ ◡ { 𝐴 } = ⟨ ( 2nd ‘ 𝐴 ) , ( 1st ‘ 𝐴 ) ⟩ )