Metamath Proof Explorer


Theorem br1cnvssrres

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

Ref Expression
Assertion br1cnvssrres
|- ( B e. V -> ( B `' ( _S |` A ) C <-> ( C e. A /\ C C_ B ) ) )

Proof

Step Hyp Ref Expression
1 relres
 |-  Rel ( _S |` A )
2 1 relbrcnv
 |-  ( B `' ( _S |` A ) C <-> C ( _S |` A ) B )
3 brssrres
 |-  ( B e. V -> ( C ( _S |` A ) B <-> ( C e. A /\ C C_ B ) ) )
4 2 3 syl5bb
 |-  ( B e. V -> ( B `' ( _S |` A ) C <-> ( C e. A /\ C C_ B ) ) )