xpopth

Description: An ordered pair theorem for members of Cartesian products. (Contributed by NM, 20-Jun-2007)

		Ref	Expression
	Assertion	xpopth	$⊢ (A \in (C \times D) \land B \in (R \times S)) \to ((1^{st} (A) = 1^{st} (B) \land 2^{nd} (A) = 2^{nd} (B)) \leftrightarrow A = B)$

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

Metamath Proof Explorer