Metamath Proof Explorer

Theorem brssrres

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

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

Proof

Step Hyp Ref Expression
1 brres 
 |-  ( C e. V -> ( B ( _S |` A ) C <-> ( B e. A /\ B _S C ) ) )
2 brssr 
 |-  ( C e. V -> ( B _S C <-> B C_ C ) )
3 2 anbi2d 
 |-  ( C e. V -> ( ( B e. A /\ B _S C ) <-> ( B e. A /\ B C_ C ) ) )
4 1 3 bitrd 
 |-  ( C e. V -> ( B ( _S |` A ) C <-> ( B e. A /\ B C_ C ) ) )