Theorem rnmptssd

Description: The range of an operation given by the maps-to notation as a subset. (Contributed by Glauco Siliprandi, 11-Oct-2020)

	Ref	Expression
Hypotheses	rnmptssd.1	|- F/ x ph
	rnmptssd.2	|- F = ( x e. A |-> B )
	rnmptssd.3	|- ( ( ph /\ x e. A ) -> B e. C )
Assertion	rnmptssd	|- ( ph -> ran F C_ C )

Proof

Step	Hyp	Ref	Expression
1		rnmptssd.1	|- F/ x ph
2		rnmptssd.2	|- F = ( x e. A |-> B )
3		rnmptssd.3	|- ( ( ph /\ x e. A ) -> B e. C )
4	1 3	ralrimia	|- ( ph -> A. x e. A B e. C )
5	2	rnmptss	|- ( A. x e. A B e. C -> ran F C_ C )
6	4 5	syl	|- ( ph -> ran F C_ C )