Metamath Proof Explorer

Theorem brcnvin

Description: Intersection with a converse, binary relation. (Contributed by Peter Mazsa, 24-Mar-2024)

Ref Expression
Assertion brcnvin ⊢ A ∈ V ∧ B ∈ W → A R ∩ S -1 B ↔ A R B ∧ B S A

Proof

Step Hyp Ref Expression
1 brin ⊢ A R ∩ S -1 B ↔ A R B ∧ A S -1 B
2 brcnvg ⊢ A ∈ V ∧ B ∈ W → A S -1 B ↔ B S A
3 2 anbi2d ⊢ A ∈ V ∧ B ∈ W → A R B ∧ A S -1 B ↔ A R B ∧ B S A
4 1 3 bitrid ⊢ A ∈ V ∧ B ∈ W → A R ∩ S -1 B ↔ A R B ∧ B S A