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 bitrid 
 |-  ( B e. V -> ( B `' ( _S |` A ) C <-> ( C e. A /\ C C_ B ) ) )