rnmpt

Description: The range of a function in maps-to notation. (Contributed by Scott Fenton, 21-Mar-2011) (Revised by Mario Carneiro, 31-Aug-2015)

		Ref	Expression
	Hypothesis	rnmpt.1	$⊢ F = (x \in A ⟼ B)$
	Assertion	rnmpt	$⊢ ran F = \{y \| \exists x \in A y = B\}$

Step	Hyp	Ref	Expression
1		rnmpt.1	$⊢ F = (x \in A ⟼ B)$
2		rnopab	$⊢ ran \{⟨x, y⟩ \| (x \in A \land y = B)\} = \{y \| \exists x (x \in A \land y = B)\}$
3		df-mpt	$⊢ (x \in A ⟼ B) = \{⟨x, y⟩ \| (x \in A \land y = B)\}$
4	1 3	eqtri	$⊢ F = \{⟨x, y⟩ \| (x \in A \land y = B)\}$
5	4	rneqi	$⊢ ran F = ran \{⟨x, y⟩ \| (x \in A \land y = B)\}$
6		df-rex	$⊢ \exists x \in A y = B \leftrightarrow \exists x (x \in A \land y = B)$
7	6	abbii	$⊢ \{y \| \exists x \in A y = B\} = \{y \| \exists x (x \in A \land y = B)\}$
8	2 5 7	3eqtr4i	$⊢ ran F = \{y \| \exists x \in A y = B\}$

Metamath Proof Explorer