Theorem 2nd1st

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

	Ref	Expression
Assertion	2nd1st	$$⊢A\in \left(B\times C\right)\to \bigcup {\left\{A\right\}}^{-1}=⟨2^{nd}\left(A\right),1^{st}\left(A\right)⟩$$

Proof

Step	Hyp	Ref	Expression
1		1st2nd2	$$⊢A\in \left(B\times C\right)\to A=⟨1^{st}\left(A\right),2^{nd}\left(A\right)⟩$$
2	1	sneqd	$$⊢A\in \left(B\times C\right)\to \left\{A\right\}=\left\{⟨1^{st}\left(A\right),2^{nd}\left(A\right)⟩\right\}$$
3	2	cnveqd	$$⊢A\in \left(B\times C\right)\to {\left\{A\right\}}^{-1}={\left\{⟨1^{st}\left(A\right),2^{nd}\left(A\right)⟩\right\}}^{-1}$$
4	3	unieqd	$$⊢A\in \left(B\times C\right)\to \bigcup {\left\{A\right\}}^{-1}=\bigcup {\left\{⟨1^{st}\left(A\right),2^{nd}\left(A\right)⟩\right\}}^{-1}$$
5		opswap	$$⊢\bigcup {\left\{⟨1^{st}\left(A\right),2^{nd}\left(A\right)⟩\right\}}^{-1}=⟨2^{nd}\left(A\right),1^{st}\left(A\right)⟩$$
6	4 5	eqtrdi	$$⊢A\in \left(B\times C\right)\to \bigcup {\left\{A\right\}}^{-1}=⟨2^{nd}\left(A\right),1^{st}\left(A\right)⟩$$