Metamath Proof Explorer


Theorem brssrres

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

Ref Expression
Assertion brssrres ( 𝐶𝑉 → ( 𝐵 ( S ↾ 𝐴 ) 𝐶 ↔ ( 𝐵𝐴𝐵𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 brres ( 𝐶𝑉 → ( 𝐵 ( S ↾ 𝐴 ) 𝐶 ↔ ( 𝐵𝐴𝐵 S 𝐶 ) ) )
2 brssr ( 𝐶𝑉 → ( 𝐵 S 𝐶𝐵𝐶 ) )
3 2 anbi2d ( 𝐶𝑉 → ( ( 𝐵𝐴𝐵 S 𝐶 ) ↔ ( 𝐵𝐴𝐵𝐶 ) ) )
4 1 3 bitrd ( 𝐶𝑉 → ( 𝐵 ( S ↾ 𝐴 ) 𝐶 ↔ ( 𝐵𝐴𝐵𝐶 ) ) )