Description: An element in the set of subcategories is a subset of the category. (Contributed by Mario Carneiro, 6-Jan-2017)
Ref | Expression | ||
---|---|---|---|
Hypotheses | subcixp.1 | |
|
subcssc.h | |
||
Assertion | subcssc | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | subcixp.1 | |
|
2 | subcssc.h | |
|
3 | eqid | |
|
4 | eqid | |
|
5 | subcrcl | |
|
6 | 1 5 | syl | |
7 | eqidd | |
|
8 | 2 3 4 6 7 | issubc | |
9 | 1 8 | mpbid | |
10 | 9 | simpld | |