Metamath Proof Explorer

Theorem brssrres

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

Ref Expression
Assertion brssrres ⊢C∈V→BS↾AC↔B∈A∧B⊆C

Proof

Step Hyp Ref Expression
1 brres ⊢C∈V→BS↾AC↔B∈A∧BSC
2 brssr ⊢C∈V→BSC↔B⊆C
3 2 anbi2d ⊢C∈V→B∈A∧BSC↔B∈A∧B⊆C
4 1 3 bitrd ⊢C∈V→BS↾AC↔B∈A∧B⊆C