This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
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 |
⊢ Funpart 𝐹 ⊆ 𝐹 |
Proof
| Step |
Hyp |
Ref |
Expression |
| 1 |
|
df-funpart |
⊢ Funpart 𝐹 = ( 𝐹 ↾ dom ( ( Image 𝐹 ∘ Singleton ) ∩ ( V × Singletons ) ) ) |
| 2 |
|
resss |
⊢ ( 𝐹 ↾ dom ( ( Image 𝐹 ∘ Singleton ) ∩ ( V × Singletons ) ) ) ⊆ 𝐹 |
| 3 |
1 2
|
eqsstri |
⊢ Funpart 𝐹 ⊆ 𝐹 |