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

Metamath Proof Explorer

Theorem opelxpi

Description: Ordered pair membership in a Cartesian product (implication). (Contributed by NM, 28-May-1995)

		Ref	Expression
	Assertion	opelxpi	$⊢ (A \in C \land B \in D) \to ⟨A, B⟩ \in (C \times D)$

Step	Hyp	Ref	Expression
1		opelxp	$⊢ ⟨A, B⟩ \in (C \times D) \leftrightarrow (A \in C \land B \in D)$
2	1	biimpri	$⊢ (A \in C \land B \in D) \to ⟨A, B⟩ \in (C \times D)$