Theorem rnmptssdf

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

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

Proof

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