Theorem cnsscnp

Description: The set of continuous functions is a subset of the set of continuous functions at a point. (Contributed by Raph Levien, 21-Oct-2006) (Revised by Mario Carneiro, 21-Aug-2015)

	Ref	Expression
Hypothesis	cnsscnp.1	|- X = U. J
Assertion	cnsscnp	|- ( P e. X -> ( J Cn K ) C_ ( ( J CnP K ) ` P ) )

Proof

Step	Hyp	Ref	Expression
1		cnsscnp.1	|- X = U. J
2	1	cncnpi	|- ( ( f e. ( J Cn K ) /\ P e. X ) -> f e. ( ( J CnP K ) ` P ) )
3	2	expcom	|- ( P e. X -> ( f e. ( J Cn K ) -> f e. ( ( J CnP K ) ` P ) ) )
4	3	ssrdv	|- ( P e. X -> ( J Cn K ) C_ ( ( J CnP K ) ` P ) )