Theorem rnmptssf

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	rnmptssf.1	⊢ Ⅎ 𝑥 𝐶
	rnmptssf.2	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
Assertion	rnmptssf	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ran 𝐹 ⊆ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		rnmptssf.1	⊢ Ⅎ 𝑥 𝐶
2		rnmptssf.2	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
3	1 2	fmptf	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 ↔ 𝐹 : 𝐴 ⟶ 𝐶 )
4		frn	⊢ ( 𝐹 : 𝐴 ⟶ 𝐶 → ran 𝐹 ⊆ 𝐶 )
5	3 4	sylbi	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ran 𝐹 ⊆ 𝐶 )