Theorem mptima

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

	Ref	Expression
Assertion	mptima	$$⊢\left(x\in A⟼B\right)\left[C\right]=\mathrm{ran}\left(x\in \left(A\cap C\right)⟼B\right)$$

Proof

Step	Hyp	Ref	Expression
1		df-ima	$$⊢\left(x\in A⟼B\right)\left[C\right]=\mathrm{ran}\left({\left(x\in A⟼B\right)\upharpoonright }_C\right)$$
2		resmpt3	$$⊢{\left(x\in A⟼B\right)\upharpoonright }_C=\left(x\in \left(A\cap C\right)⟼B\right)$$
3	2	rneqi	$$⊢\mathrm{ran}\left({\left(x\in A⟼B\right)\upharpoonright }_C\right)=\mathrm{ran}\left(x\in \left(A\cap C\right)⟼B\right)$$
4	1 3	eqtri	$$⊢\left(x\in A⟼B\right)\left[C\right]=\mathrm{ran}\left(x\in \left(A\cap C\right)⟼B\right)$$