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 x y | ψ A V × V

Proof

Step Hyp Ref Expression
1 vex x V
2 vex y V
3 1 2 pm3.2i x V y V
4 3 a1i ψ x V y V
5 4 ssopab2i x y | ψ x y | x V y V
6 df-xp V × V = x y | x V y V
7 5 6 sseqtrri x y | ψ V × V
8 7 sseli A x y | ψ A V × V