Metamath Proof Explorer

Theorem brin

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

Ref Expression
Assertion brin ⊢ A R ∩ S B ↔ A R B ∧ A S B

Proof

Step Hyp Ref Expression
1 elin ⊢ A B ∈ R ∩ S ↔ A B ∈ R ∧ A B ∈ S
2 df-br ⊢ A R ∩ S B ↔ A B ∈ R ∩ S
3 df-br ⊢ A R B ↔ A B ∈ R
4 df-br ⊢ A S B ↔ A B ∈ S
5 3 4 anbi12i ⊢ A R B ∧ A S B ↔ A B ∈ R ∧ A B ∈ S
6 1 2 5 3bitr4i ⊢ A R ∩ S B ↔ A R B ∧ A S B