Theorem funpartss

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 𝐹 ⊆ 𝐹