This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mptima

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

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

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