Metamath Proof Explorer


Theorem br1cnvssrres

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

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

Proof

Step Hyp Ref Expression
1 relres Rel ( S ↾ 𝐴 )
2 1 relbrcnv ( 𝐵 ( S ↾ 𝐴 ) 𝐶𝐶 ( S ↾ 𝐴 ) 𝐵 )
3 brssrres ( 𝐵𝑉 → ( 𝐶 ( S ↾ 𝐴 ) 𝐵 ↔ ( 𝐶𝐴𝐶𝐵 ) ) )
4 2 3 syl5bb ( 𝐵𝑉 → ( 𝐵 ( S ↾ 𝐴 ) 𝐶 ↔ ( 𝐶𝐴𝐶𝐵 ) ) )