Metamath Proof Explorer

Theorem brinxp2

Description: Intersection of binary relation with Cartesian product. (Contributed by NM, 3-Mar-2007) (Revised by Mario Carneiro, 26-Apr-2015) Group conjuncts and avoid df-3an . (Revised by Peter Mazsa, 18-Sep-2022)

		Ref	Expression
	Assertion	brinxp2	$⊢ C (R \cap (A \times B)) D \leftrightarrow ((C \in A \land D \in B) \land C R D)$

Proof

Step	Hyp	Ref	Expression
1		brin	$⊢ C (R \cap (A \times B)) D \leftrightarrow (C R D \land C (A \times B) D)$
2		ancom	$⊢ (C R D \land C (A \times B) D) \leftrightarrow (C (A \times B) D \land C R D)$
3		brxp	$⊢ C (A \times B) D \leftrightarrow (C \in A \land D \in B)$
4	3	anbi1i	$⊢ (C (A \times B) D \land C R D) \leftrightarrow ((C \in A \land D \in B) \land C R D)$
5	1 2 4	3bitri	$⊢ C (R \cap (A \times B)) D \leftrightarrow ((C \in A \land D \in B) \land C R D)$