xp2

Description: Representation of Cartesian product based on ordered pair component functions. (Contributed by NM, 16-Sep-2006)

		Ref	Expression
	Assertion	xp2	$⊢ A \times B = \{x \in (V \times V) \| (1^{st} (x) \in A \land 2^{nd} (x) \in B)\}$

Step	Hyp	Ref	Expression
1		elxp7	$⊢ x \in (A \times B) \leftrightarrow (x \in (V \times V) \land (1^{st} (x) \in A \land 2^{nd} (x) \in B))$
2	1	eqabi	$⊢ A \times B = \{x \| (x \in (V \times V) \land (1^{st} (x) \in A \land 2^{nd} (x) \in B))\}$
3		df-rab	$⊢ \{x \in (V \times V) \| (1^{st} (x) \in A \land 2^{nd} (x) \in B)\} = \{x \| (x \in (V \times V) \land (1^{st} (x) \in A \land 2^{nd} (x) \in B))\}$
4	2 3	eqtr4i	$⊢ A \times B = \{x \in (V \times V) \| (1^{st} (x) \in A \land 2^{nd} (x) \in B)\}$

Metamath Proof Explorer