Metamath Proof Explorer

Theorem brin2

Description: Binary relation on an intersection is a special case of binary relation on range Cartesian product. (Contributed by Peter Mazsa, 21-Aug-2021)

Ref Expression
Assertion brin2 ⊢ A ∈ V ∧ B ∈ W → A R ∩ S B ↔ A R ⋉ S B B

Proof

Step Hyp Ref Expression
1 brin ⊢ A R ∩ S B ↔ A R B ∧ A S B
2 brxrn ⊢ A ∈ V ∧ B ∈ W ∧ B ∈ W → A R ⋉ S B B ↔ A R B ∧ A S B
3 2 3anidm23 ⊢ A ∈ V ∧ B ∈ W → A R ⋉ S B B ↔ A R B ∧ A S B
4 1 3 bitr4id ⊢ A ∈ V ∧ B ∈ W → A R ∩ S B ↔ A R ⋉ S B B