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)

Ref Expression
Assertion elopaelxp ( 𝐴 ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } → 𝐴 ∈ ( V × V ) )

Proof

Step Hyp Ref Expression
1 simpl ( ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜓 ) → 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ )
2 1 2eximi ( ∃ 𝑥𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜓 ) → ∃ 𝑥𝑦 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ )
3 elopab ( 𝐴 ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ↔ ∃ 𝑥𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜓 ) )
4 elvv ( 𝐴 ∈ ( V × V ) ↔ ∃ 𝑥𝑦 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ )
5 2 3 4 3imtr4i ( 𝐴 ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } → 𝐴 ∈ ( V × V ) )