Description: Restricted converse subset binary relation. (Contributed by Peter Mazsa, 25-Nov-2019)
Ref | Expression | ||
---|---|---|---|
Assertion | br1cnvssrres | ⊢ ( 𝐵 ∈ 𝑉 → ( 𝐵 ◡ ( S ↾ 𝐴 ) 𝐶 ↔ ( 𝐶 ∈ 𝐴 ∧ 𝐶 ⊆ 𝐵 ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | relres | ⊢ Rel ( S ↾ 𝐴 ) | |
2 | 1 | relbrcnv | ⊢ ( 𝐵 ◡ ( S ↾ 𝐴 ) 𝐶 ↔ 𝐶 ( S ↾ 𝐴 ) 𝐵 ) |
3 | brssrres | ⊢ ( 𝐵 ∈ 𝑉 → ( 𝐶 ( S ↾ 𝐴 ) 𝐵 ↔ ( 𝐶 ∈ 𝐴 ∧ 𝐶 ⊆ 𝐵 ) ) ) | |
4 | 2 3 | syl5bb | ⊢ ( 𝐵 ∈ 𝑉 → ( 𝐵 ◡ ( S ↾ 𝐴 ) 𝐶 ↔ ( 𝐶 ∈ 𝐴 ∧ 𝐶 ⊆ 𝐵 ) ) ) |