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 | |- Funpart F C_ F |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-funpart | |- Funpart F = ( F |` dom ( ( Image F o. Singleton ) i^i ( _V X. Singletons ) ) ) |
|
2 | resss | |- ( F |` dom ( ( Image F o. Singleton ) i^i ( _V X. Singletons ) ) ) C_ F |
|
3 | 1 2 | eqsstri | |- Funpart F C_ F |