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 CVBRACBABRC

Proof

Step Hyp Ref Expression
1 opelres CVBCRABABCR
2 df-br BRACBCRA
3 df-br BRCBCR
4 3 anbi2i BABRCBABCR
5 1 2 4 3bitr4g CVBRACBABRC