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

Metamath Proof Explorer

Theorem opelvvg

Description: Ordered pair membership in the universal class of ordered pairs. (Contributed by Mario Carneiro, 3-May-2015)

		Ref	Expression
	Assertion	opelvvg	$⊢ (A \in V \land B \in W) \to ⟨A, B⟩ \in (V \times V)$

Step	Hyp	Ref	Expression
1		elex	$⊢ A \in V \to A \in V$
2		elex	$⊢ B \in W \to B \in V$
3		opelxpi	$⊢ (A \in V \land B \in V) \to ⟨A, B⟩ \in (V \times V)$
4	1 2 3	syl2an	$⊢ (A \in V \land B \in W) \to ⟨A, B⟩ \in (V \times V)$