Theorem elopaelxp

Description: Membership in an ordered pair class builder 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 ) )