# Metamath Proof Explorer

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}\left[\mathrm{dom}{A}\right]=\mathrm{ran}{A}$

### Proof

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