Theorem rnmptssff

Description: The range of a function given by the maps-to notation as a subset. (Contributed by Glauco Siliprandi, 24-Jan-2025)

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

Proof

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