eqop2

Description: Two ways to express equality with an ordered pair. (Contributed by NM, 25-Feb-2014)

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

Step	Hyp	Ref	Expression
1		eqop2.1	$⊢ B \in V$
2		eqop2.2	$⊢ C \in V$
3	1 2	opelvv	$⊢ ⟨B, C⟩ \in (V \times V)$
4		eleq1	$⊢ A = ⟨B, C⟩ \to (A \in (V \times V) \leftrightarrow ⟨B, C⟩ \in (V \times V))$
5	3 4	mpbiri	$⊢ A = ⟨B, C⟩ \to A \in (V \times V)$
6		eqop	$⊢ A \in (V \times V) \to (A = ⟨B, C⟩ \leftrightarrow (1^{st} (A) = B \land 2^{nd} (A) = C))$
7	5 6	biadanii	$⊢ A = ⟨B, C⟩ \leftrightarrow (A \in (V \times V) \land (1^{st} (A) = B \land 2^{nd} (A) = C))$

Metamath Proof Explorer