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