Metamath Proof Explorer


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 ) }