brin

Description: The intersection of two relations. (Contributed by FL, 7-Oct-2008)

		Ref	Expression
	Assertion	brin	$⊢ A (R \cap S) B \leftrightarrow (A R B \land A S B)$

Step	Hyp	Ref	Expression
1		elin	$⊢ ⟨A, B⟩ \in (R \cap S) \leftrightarrow (⟨A, B⟩ \in R \land ⟨A, B⟩ \in S)$
2		df-br	$⊢ A (R \cap S) B \leftrightarrow ⟨A, B⟩ \in (R \cap S)$
3		df-br	$⊢ A R B \leftrightarrow ⟨A, B⟩ \in R$
4		df-br	$⊢ A S B \leftrightarrow ⟨A, B⟩ \in S$
5	3 4	anbi12i	$⊢ (A R B \land A S B) \leftrightarrow (⟨A, B⟩ \in R \land ⟨A, B⟩ \in S)$
6	1 2 5	3bitr4i	$⊢ A (R \cap S) B \leftrightarrow (A R B \land A S B)$

Metamath Proof Explorer