Metamath Proof Explorer


Theorem elopaelxp

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

Proof

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