# Metamath Proof Explorer

## Theorem imai

Description: Image under the identity relation. Theorem 3.16(viii) of Monk1 p. 38. (Contributed by NM, 30-Apr-1998)

Ref Expression
Assertion imai ${⊢}\mathrm{I}\left[{A}\right]={A}$

### Proof

Step Hyp Ref Expression
1 dfima3 ${⊢}\mathrm{I}\left[{A}\right]=\left\{{y}|\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge ⟨{x},{y}⟩\in \mathrm{I}\right)\right\}$
2 df-br ${⊢}{x}\mathrm{I}{y}↔⟨{x},{y}⟩\in \mathrm{I}$
3 vex ${⊢}{y}\in \mathrm{V}$
4 3 ideq ${⊢}{x}\mathrm{I}{y}↔{x}={y}$
5 2 4 bitr3i ${⊢}⟨{x},{y}⟩\in \mathrm{I}↔{x}={y}$
6 5 anbi1ci ${⊢}\left({x}\in {A}\wedge ⟨{x},{y}⟩\in \mathrm{I}\right)↔\left({x}={y}\wedge {x}\in {A}\right)$
7 6 exbii ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge ⟨{x},{y}⟩\in \mathrm{I}\right)↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\wedge {x}\in {A}\right)$
8 eleq1w ${⊢}{x}={y}\to \left({x}\in {A}↔{y}\in {A}\right)$
9 8 equsexvw ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\wedge {x}\in {A}\right)↔{y}\in {A}$
10 7 9 bitri ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge ⟨{x},{y}⟩\in \mathrm{I}\right)↔{y}\in {A}$
11 10 abbii ${⊢}\left\{{y}|\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge ⟨{x},{y}⟩\in \mathrm{I}\right)\right\}=\left\{{y}|{y}\in {A}\right\}$
12 abid2 ${⊢}\left\{{y}|{y}\in {A}\right\}={A}$
13 1 11 12 3eqtri ${⊢}\mathrm{I}\left[{A}\right]={A}$