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