imadmrn

Description: The image of the domain of a class is the range of the class. (Contributed by NM, 14-Aug-1994)

		Ref	Expression
	Assertion	imadmrn	$⊢ A [dom A] = ran A$

Step	Hyp	Ref	Expression
1		vex	$⊢ x \in V$
2		vex	$⊢ y \in V$
3	1 2	opeldm	$⊢ ⟨x, y⟩ \in A \to x \in dom A$
4	3	pm4.71i	$⊢ ⟨x, y⟩ \in A \leftrightarrow (⟨x, y⟩ \in A \land x \in dom A)$
5		ancom	$⊢ (⟨x, y⟩ \in A \land x \in dom A) \leftrightarrow (x \in dom A \land ⟨x, y⟩ \in A)$
6	4 5	bitr2i	$⊢ (x \in dom A \land ⟨x, y⟩ \in A) \leftrightarrow ⟨x, y⟩ \in A$
7	6	exbii	$⊢ \exists x (x \in dom A \land ⟨x, y⟩ \in A) \leftrightarrow \exists x ⟨x, y⟩ \in A$
8	7	abbii	$⊢ \{y \| \exists x (x \in dom A \land ⟨x, y⟩ \in A)\} = \{y \| \exists x ⟨x, y⟩ \in A\}$
9		dfima3	$⊢ A [dom A] = \{y \| \exists x (x \in dom A \land ⟨x, y⟩ \in A)\}$
10		dfrn3	$⊢ ran A = \{y \| \exists x ⟨x, y⟩ \in A\}$
11	8 9 10	3eqtr4i	$⊢ A [dom A] = ran A$

Metamath Proof Explorer