Metamath Proof Explorer


Theorem brssrres

Description: Restricted subset binary relation. (Contributed by Peter Mazsa, 25-Nov-2019)

Ref Expression
Assertion brssrres C V B S A C B A B C

Proof

Step Hyp Ref Expression
1 brres C V B S A C B A B S C
2 brssr C V B S C B C
3 2 anbi2d C V B A B S C B A B C
4 1 3 bitrd C V B S A C B A B C