eqopi

Description: Equality with an ordered pair. (Contributed by NM, 15-Dec-2008) (Revised by Mario Carneiro, 23-Feb-2014)

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

Step	Hyp	Ref	Expression
1		xpss	$⊢ V \times W \subseteq V \times V$
2	1	sseli	$⊢ A \in (V \times W) \to A \in (V \times V)$
3		elxp6	$⊢ A \in (V \times V) \leftrightarrow (A = ⟨1^{st} (A), 2^{nd} (A)⟩ \land (1^{st} (A) \in V \land 2^{nd} (A) \in V))$
4	3	simplbi	$⊢ A \in (V \times V) \to A = ⟨1^{st} (A), 2^{nd} (A)⟩$
5		opeq12	$⊢ (1^{st} (A) = B \land 2^{nd} (A) = C) \to ⟨1^{st} (A), 2^{nd} (A)⟩ = ⟨B, C⟩$
6	4 5	sylan9eq	$⊢ (A \in (V \times V) \land (1^{st} (A) = B \land 2^{nd} (A) = C)) \to A = ⟨B, C⟩$
7	2 6	sylan	$⊢ (A \in (V \times W) \land (1^{st} (A) = B \land 2^{nd} (A) = C)) \to A = ⟨B, C⟩$

Metamath Proof Explorer