Theorem mptimass

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

	Ref	Expression
Hypothesis	mptimass.1	$$⊢\phi \to C\subseteq A$$
Assertion	mptimass	$$⊢\phi \to \left(x\in A⟼B\right)\left[C\right]=\mathrm{ran}\left(x\in C⟼B\right)$$

Proof

Step	Hyp	Ref	Expression
1		mptimass.1	$$⊢\phi \to C\subseteq A$$
2		mptima	$$⊢\left(x\in A⟼B\right)\left[C\right]=\mathrm{ran}\left(x\in \left(A\cap C\right)⟼B\right)$$
3		sseqin2	$$⊢C\subseteq A\leftrightarrow A\cap C=C$$
4	1 3	sylib	$$⊢\phi \to A\cap C=C$$
5	4	mpteq1d	$$⊢\phi \to \left(x\in \left(A\cap C\right)⟼B\right)=\left(x\in C⟼B\right)$$
6	5	rneqd	$$⊢\phi \to \mathrm{ran}\left(x\in \left(A\cap C\right)⟼B\right)=\mathrm{ran}\left(x\in C⟼B\right)$$
7	2 6	eqtrid	$$⊢\phi \to \left(x\in A⟼B\right)\left[C\right]=\mathrm{ran}\left(x\in C⟼B\right)$$