This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 \in \{⟨x, y⟩ \| ψ\} \to A \in (V \times V)$

Proof

Step	Hyp	Ref	Expression
1		vex	$⊢ x \in V$
2		vex	$⊢ y \in V$
3	1 2	pm3.2i	$⊢ (x \in V \land y \in V)$
4	3	a1i	$⊢ ψ \to (x \in V \land y \in V)$
5	4	ssopab2i	$⊢ \{⟨x, y⟩ \| ψ\} \subseteq \{⟨x, y⟩ \| (x \in V \land y \in V)\}$
6		df-xp	$⊢ V \times V = \{⟨x, y⟩ \| (x \in V \land y \in V)\}$
7	5 6	sseqtrri	$⊢ \{⟨x, y⟩ \| ψ\} \subseteq V \times V$
8	7	sseli	$⊢ A \in \{⟨x, y⟩ \| ψ\} \to A \in (V \times V)$