Theorem mptima

Description: Image of a function in maps-to notation. (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Assertion	mptima	⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) “ 𝐶 ) = ran ( 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ↦ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		df-ima	⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) “ 𝐶 ) = ran ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝐶 )
2		resmpt3	⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝐶 ) = ( 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ↦ 𝐵 )
3	2	rneqi	⊢ ran ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝐶 ) = ran ( 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ↦ 𝐵 )
4	1 3	eqtri	⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) “ 𝐶 ) = ran ( 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ↦ 𝐵 )