Metamath Proof Explorer


Theorem brinxprnres

Description: Binary relation on a restriction. (Contributed by Peter Mazsa, 2-Jan-2019)

Ref Expression
Assertion brinxprnres C V B R A × ran R A C B A B R C

Proof

Step Hyp Ref Expression
1 brres2 B R A C B R A × ran R A C
2 brres C V B R A C B A B R C
3 1 2 bitr3id C V B R A × ran R A C B A B R C