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

Metamath Proof Explorer

Theorem fnasrn

Description: A function expressed as the range of another function. (Contributed by Mario Carneiro, 22-Jun-2013) (Proof shortened by Mario Carneiro, 31-Aug-2015)

		Ref	Expression
	Hypothesis	dfmpt.1	$⊢ B \in V$
	Assertion	fnasrn	$⊢ (x \in A ⟼ B) = ran (x \in A ⟼ ⟨x, B⟩)$

Proof

Step	Hyp	Ref	Expression
1		dfmpt.1	$⊢ B \in V$
2	1	dfmpt	$⊢ (x \in A ⟼ B) = ⋃_{x \in A} \{⟨x, B⟩\}$
3		eqid	$⊢ (x \in A ⟼ ⟨x, B⟩) = (x \in A ⟼ ⟨x, B⟩)$
4	3	rnmpt	$⊢ ran (x \in A ⟼ ⟨x, B⟩) = \{y \| \exists x \in A y = ⟨x, B⟩\}$
5		velsn	$⊢ y \in \{⟨x, B⟩\} \leftrightarrow y = ⟨x, B⟩$
6	5	rexbii	$⊢ \exists x \in A y \in \{⟨x, B⟩\} \leftrightarrow \exists x \in A y = ⟨x, B⟩$
7	6	abbii	$⊢ \{y \| \exists x \in A y \in \{⟨x, B⟩\}\} = \{y \| \exists x \in A y = ⟨x, B⟩\}$
8	4 7	eqtr4i	$⊢ ran (x \in A ⟼ ⟨x, B⟩) = \{y \| \exists x \in A y \in \{⟨x, B⟩\}\}$
9		df-iun	$⊢ ⋃_{x \in A} \{⟨x, B⟩\} = \{y \| \exists x \in A y \in \{⟨x, B⟩\}\}$
10	8 9	eqtr4i	$⊢ ran (x \in A ⟼ ⟨x, B⟩) = ⋃_{x \in A} \{⟨x, B⟩\}$
11	2 10	eqtr4i	$⊢ (x \in A ⟼ B) = ran (x \in A ⟼ ⟨x, B⟩)$