Metamath Proof Explorer
Description: The base set of a restriction to A is a subset of A .
(Contributed by SN, 10-Jan-2025)
|
|
Ref |
Expression |
|
Hypothesis |
ressbasss2.r |
|
|
Assertion |
ressbasss2 |
|
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
ressbasss2.r |
|
2 |
|
eqid |
|
3 |
1 2
|
ressbasssg |
|
4 |
|
inss1 |
|
5 |
3 4
|
sstri |
|