Theorem opelxpi

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

	Ref	Expression
Assertion	opelxpi	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝐶 × 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		opelxp	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝐶 × 𝐷 ) ↔ ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) )
2	1	biimpri	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝐶 × 𝐷 ) )