Theorem rnmptss2

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	rnmptss2.1	⊢ Ⅎ 𝑥 𝜑
	rnmptss2.3	⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
	rnmptss2.4	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ 𝑉 )
Assertion	rnmptss2	⊢ ( 𝜑 → ran ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ⊆ ran ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		rnmptss2.1	⊢ Ⅎ 𝑥 𝜑
2		rnmptss2.3	⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
3		rnmptss2.4	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ 𝑉 )
4		nfmpt1	⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝐵 ↦ 𝐶 )
5	4	nfrn	⊢ Ⅎ 𝑥 ran ( 𝑥 ∈ 𝐵 ↦ 𝐶 )
6		eqid	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐶 )
7		eqid	⊢ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) = ( 𝑥 ∈ 𝐵 ↦ 𝐶 )
8	2	sselda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐵 )
9	7 8 3	elrnmpt1d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ran ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) )
10	1 5 6 9	rnmptssdf	⊢ ( 𝜑 → ran ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ⊆ ran ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) )