This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 1st2nd2

Description: Reconstruction of a member of a Cartesian product in terms of its ordered pair components. (Contributed by NM, 20-Oct-2013)

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

Step	Hyp	Ref	Expression
1		elxp6	$⊢ A \in (B \times C) \leftrightarrow (A = ⟨1^{st} (A), 2^{nd} (A)⟩ \land (1^{st} (A) \in B \land 2^{nd} (A) \in C))$
2	1	simplbi	$⊢ A \in (B \times C) \to A = ⟨1^{st} (A), 2^{nd} (A)⟩$