Description: Ordered pair membership in a Cartesian product (implication). (Contributed by Steven Nguyen, 17-Jul-2022)
Ref | Expression | ||
---|---|---|---|
Hypotheses | opelxpii.1 | |- A e. C |
|
opelxpii.2 | |- B e. D |
||
Assertion | opelxpii | |- <. A , B >. e. ( C X. D ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | opelxpii.1 | |- A e. C |
|
2 | opelxpii.2 | |- B e. D |
|
3 | opelxpi | |- ( ( A e. C /\ B e. D ) -> <. A , B >. e. ( C X. D ) ) |
|
4 | 1 2 3 | mp2an | |- <. A , B >. e. ( C X. D ) |