Metamath Proof Explorer


Theorem br1cnvssrres

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

Ref Expression
Assertion br1cnvssrres B V B S A -1 C C A C B

Proof

Step Hyp Ref Expression
1 relres Rel S A
2 1 relbrcnv B S A -1 C C S A B
3 brssrres B V C S A B C A C B
4 2 3 syl5bb B V B S A -1 C C A C B