Theorem opelxpi

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

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

Proof

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