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\left(x\in A\wedge ⟨x,y⟩\in \mathrm{I}\right)\right\}$$
2		df-br	$$⊢x\mathrm{I}y\leftrightarrow ⟨x,y⟩\in \mathrm{I}$$
3		vex	$$⊢y\in \mathrm{V}$$
4	3	ideq	$$⊢x\mathrm{I}y\leftrightarrow x=y$$
5	2 4	bitr3i	$$⊢⟨x,y⟩\in \mathrm{I}\leftrightarrow x=y$$
6	5	anbi1ci	$$⊢\left(x\in A\wedge ⟨x,y⟩\in \mathrm{I}\right)\leftrightarrow \left(x=y\wedge x\in A\right)$$
7	6	exbii	$$⊢\exists x\left(x\in A\wedge ⟨x,y⟩\in \mathrm{I}\right)\leftrightarrow \exists x\left(x=y\wedge x\in A\right)$$
8		eleq1w	$$⊢x=y\to \left(x\in A\leftrightarrow y\in A\right)$$
9	8	equsexvw	$$⊢\exists x\left(x=y\wedge x\in A\right)\leftrightarrow y\in A$$
10	7 9	bitri	$$⊢\exists x\left(x\in A\wedge ⟨x,y⟩\in \mathrm{I}\right)\leftrightarrow y\in A$$
11	10	abbii	$$⊢\left\{y|\exists x\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$$