Theorem rnmptss

Description: The range of an operation given by the maps-to notation as a subset. (Contributed by Thierry Arnoux, 24-Sep-2017)

	Ref	Expression
Hypothesis	rnmptss.1	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
Assertion	rnmptss	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ran 𝐹 ⊆ 𝐶 )

Proof

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