Metamath Proof Explorer

Theorem brssrres

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

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

Proof

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