Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Peter Mazsa
Subset relations
relssr
Next ⟩
brssr
Metamath Proof Explorer
Ascii
Unicode
Theorem
relssr
Description:
The subset relation is a relation.
(Contributed by
Peter Mazsa
, 1-Aug-2019)
Ref
Expression
Assertion
relssr
⊢
Rel
⁡
S
Proof
Step
Hyp
Ref
Expression
1
df-ssr
⊢
S
=
x
y
|
x
⊆
y
2
1
relopabiv
⊢
Rel
⁡
S