Theorem 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=\left\{x\in \left(\mathrm{V}\times \mathrm{V}\right)|\left(1^{st}\left(x\right)\in A\wedge 2^{nd}\left(x\right)\in B\right)\right\}$$

Proof

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