Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Peter Mazsa
Subset relations
br1cnvssrres
Next ⟩
brcnvssr
Metamath Proof Explorer
Ascii
Unicode
Theorem
br1cnvssrres
Description:
Restricted converse subset binary relation.
(Contributed by
Peter Mazsa
, 25-Nov-2019)
Ref
Expression
Assertion
br1cnvssrres
⊢
B
∈
V
→
B
S
↾
A
-1
C
↔
C
∈
A
∧
C
⊆
B
Proof
Step
Hyp
Ref
Expression
1
relres
⊢
Rel
⁡
S
↾
A
2
1
relbrcnv
⊢
B
S
↾
A
-1
C
↔
C
S
↾
A
B
3
brssrres
⊢
B
∈
V
→
C
S
↾
A
B
↔
C
∈
A
∧
C
⊆
B
4
2
3
syl5bb
⊢
B
∈
V
→
B
S
↾
A
-1
C
↔
C
∈
A
∧
C
⊆
B