opelinxp

Description: Ordered pair element in an intersection with Cartesian product. (Contributed by Peter Mazsa, 21-Jul-2019)

		Ref	Expression
	Assertion	opelinxp	$⊢ ⟨C, D⟩ \in (R \cap (A \times B)) \leftrightarrow ((C \in A \land D \in B) \land ⟨C, D⟩ \in R)$

Step	Hyp	Ref	Expression
1		brinxp2	$⊢ C (R \cap (A \times B)) D \leftrightarrow ((C \in A \land D \in B) \land C R D)$
2		df-br	$⊢ C (R \cap (A \times B)) D \leftrightarrow ⟨C, D⟩ \in (R \cap (A \times B))$
3		df-br	$⊢ C R D \leftrightarrow ⟨C, D⟩ \in R$
4	3	anbi2i	$⊢ ((C \in A \land D \in B) \land C R D) \leftrightarrow ((C \in A \land D \in B) \land ⟨C, D⟩ \in R)$
5	1 2 4	3bitr3i	$⊢ ⟨C, D⟩ \in (R \cap (A \times B)) \leftrightarrow ((C \in A \land D \in B) \land ⟨C, D⟩ \in R)$

Metamath Proof Explorer