Theorem mptss

Description: Sufficient condition for inclusion among two functions in maps-to notation. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Assertion	mptss	⊢ ( 𝐴 ⊆ 𝐵 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ⊆ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		resmpt	⊢ ( 𝐴 ⊆ 𝐵 → ( ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ↾ 𝐴 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) )
2		resss	⊢ ( ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ↾ 𝐴 ) ⊆ ( 𝑥 ∈ 𝐵 ↦ 𝐶 )
3	1 2	eqsstrrdi	⊢ ( 𝐴 ⊆ 𝐵 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ⊆ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) )