Metamath Proof Explorer
Description: The functional part of F is a subset of F . (Contributed by Scott
Fenton, 17-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)
|
|
Ref |
Expression |
|
Assertion |
funpartss |
|
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
df-funpart |
|
2 |
|
resss |
|
3 |
1 2
|
eqsstri |
|