Metamath Proof Explorer


Theorem brres

Description: Binary relation on a restriction. (Contributed by Mario Carneiro, 4-Nov-2015) Commute the consequent. (Revised by Peter Mazsa, 24-Sep-2022)

Ref Expression
Assertion brres ( 𝐶𝑉 → ( 𝐵 ( 𝑅𝐴 ) 𝐶 ↔ ( 𝐵𝐴𝐵 𝑅 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 opelres ( 𝐶𝑉 → ( ⟨ 𝐵 , 𝐶 ⟩ ∈ ( 𝑅𝐴 ) ↔ ( 𝐵𝐴 ∧ ⟨ 𝐵 , 𝐶 ⟩ ∈ 𝑅 ) ) )
2 df-br ( 𝐵 ( 𝑅𝐴 ) 𝐶 ↔ ⟨ 𝐵 , 𝐶 ⟩ ∈ ( 𝑅𝐴 ) )
3 df-br ( 𝐵 𝑅 𝐶 ↔ ⟨ 𝐵 , 𝐶 ⟩ ∈ 𝑅 )
4 3 anbi2i ( ( 𝐵𝐴𝐵 𝑅 𝐶 ) ↔ ( 𝐵𝐴 ∧ ⟨ 𝐵 , 𝐶 ⟩ ∈ 𝑅 ) )
5 1 2 4 3bitr4g ( 𝐶𝑉 → ( 𝐵 ( 𝑅𝐴 ) 𝐶 ↔ ( 𝐵𝐴𝐵 𝑅 𝐶 ) ) )