2nd1st

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

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

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

Metamath Proof Explorer