eqop

Description: Two ways to express equality with an ordered pair. (Contributed by NM, 3-Sep-2007) (Proof shortened by Mario Carneiro, 26-Apr-2015)

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

Step	Hyp	Ref	Expression
1		1st2nd2	$⊢ A \in (V \times W) \to A = ⟨1^{st} (A), 2^{nd} (A)⟩$
2	1	eqeq1d	$⊢ A \in (V \times W) \to (A = ⟨B, C⟩ \leftrightarrow ⟨1^{st} (A), 2^{nd} (A)⟩ = ⟨B, C⟩)$
3		fvex	$⊢ 1^{st} (A) \in V$
4		fvex	$⊢ 2^{nd} (A) \in V$
5	3 4	opth	$⊢ ⟨1^{st} (A), 2^{nd} (A)⟩ = ⟨B, C⟩ \leftrightarrow (1^{st} (A) = B \land 2^{nd} (A) = C)$
6	2 5	bitrdi	$⊢ A \in (V \times W) \to (A = ⟨B, C⟩ \leftrightarrow (1^{st} (A) = B \land 2^{nd} (A) = C))$

Metamath Proof Explorer