Theorem rnmptssd

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

	Ref	Expression
Hypotheses	rnmptssd.1	⊢ Ⅎ 𝑥 𝜑
	rnmptssd.2	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
	rnmptssd.3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝐶 )
Assertion	rnmptssd	⊢ ( 𝜑 → ran 𝐹 ⊆ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		rnmptssd.1	⊢ Ⅎ 𝑥 𝜑
2		rnmptssd.2	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
3		rnmptssd.3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝐶 )
4	1 3	ralrimia	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 )
5	2	rnmptss	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ran 𝐹 ⊆ 𝐶 )
6	4 5	syl	⊢ ( 𝜑 → ran 𝐹 ⊆ 𝐶 )