Description: Membership in an ordered-pair class abstraction implies membership in a Cartesian product. (Contributed by Alexander van der Vekens, 23-Jun-2018) Avoid ax-sep , ax-nul , ax-pr . (Revised by SN, 11-Dec-2024)
Ref | Expression | ||
---|---|---|---|
Assertion | elopaelxp | |- ( A e. { <. x , y >. | ps } -> A e. ( _V X. _V ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vex | |- x e. _V |
|
2 | vex | |- y e. _V |
|
3 | 1 2 | pm3.2i | |- ( x e. _V /\ y e. _V ) |
4 | 3 | a1i | |- ( ps -> ( x e. _V /\ y e. _V ) ) |
5 | 4 | ssopab2i | |- { <. x , y >. | ps } C_ { <. x , y >. | ( x e. _V /\ y e. _V ) } |
6 | df-xp | |- ( _V X. _V ) = { <. x , y >. | ( x e. _V /\ y e. _V ) } |
|
7 | 5 6 | sseqtrri | |- { <. x , y >. | ps } C_ ( _V X. _V ) |
8 | 7 | sseli | |- ( A e. { <. x , y >. | ps } -> A e. ( _V X. _V ) ) |