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 ⊢ C ∈ V → B R ↾ A C ↔ B ∈ A ∧ B R C

Proof

Step Hyp Ref Expression
1 opelres ⊢ C ∈ V → B C ∈ R ↾ A ↔ B ∈ A ∧ B C ∈ R
2 df-br ⊢ B R ↾ A C ↔ B C ∈ R ↾ A
3 df-br ⊢ B R C ↔ B C ∈ R
4 3 anbi2i ⊢ B ∈ A ∧ B R C ↔ B ∈ A ∧ B C ∈ R
5 1 2 4 3bitr4g ⊢ C ∈ V → B R ↾ A C ↔ B ∈ A ∧ B R C