Theorem xp2

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

	Ref	Expression
Assertion	xp2	|- ( A X. B ) = { x e. ( _V X. _V ) | ( ( 1st ` x ) e. A /\ ( 2nd ` x ) e. B ) }

Proof

Step	Hyp	Ref	Expression
1		elxp7	|- ( x e. ( A X. B ) <-> ( x e. ( _V X. _V ) /\ ( ( 1st ` x ) e. A /\ ( 2nd ` x ) e. B ) ) )
2	1	abbi2i	|- ( A X. B ) = { x | ( x e. ( _V X. _V ) /\ ( ( 1st ` x ) e. A /\ ( 2nd ` x ) e. B ) ) }
3		df-rab	|- { x e. ( _V X. _V ) | ( ( 1st ` x ) e. A /\ ( 2nd ` x ) e. B ) } = { x | ( x e. ( _V X. _V ) /\ ( ( 1st ` x ) e. A /\ ( 2nd ` x ) e. B ) ) }
4	2 3	eqtr4i	|- ( A X. B ) = { x e. ( _V X. _V ) | ( ( 1st ` x ) e. A /\ ( 2nd ` x ) e. B ) }