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 ( 𝐴 ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } → 𝐴 ∈ ( V × V ) )

Proof

Step Hyp Ref Expression
1 vex 𝑥 ∈ V
2 vex 𝑦 ∈ V
3 1 2 pm3.2i ( 𝑥 ∈ V ∧ 𝑦 ∈ V )
4 3 a1i ( 𝜓 → ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) )
5 4 ssopab2i { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ⊆ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) }
6 df-xp ( V × V ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) }
7 5 6 sseqtrri { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ⊆ ( V × V )
8 7 sseli ( 𝐴 ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } → 𝐴 ∈ ( V × V ) )