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 ↾ 𝐴 ) 𝐶 ↔ ( 𝐵 ∈ 𝐴 ∧ 𝐵 ⊆ 𝐶 ) ) )