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
|- ( _I " A ) = A

Proof

Step Hyp Ref Expression
1 dfima3
 |-  ( _I " A ) = { y | E. x ( x e. A /\ <. x , y >. e. _I ) }
2 df-br
 |-  ( x _I y <-> <. x , y >. e. _I )
3 vex
 |-  y e. _V
4 3 ideq
 |-  ( x _I y <-> x = y )
5 2 4 bitr3i
 |-  ( <. x , y >. e. _I <-> x = y )
6 5 anbi1ci
 |-  ( ( x e. A /\ <. x , y >. e. _I ) <-> ( x = y /\ x e. A ) )
7 6 exbii
 |-  ( E. x ( x e. A /\ <. x , y >. e. _I ) <-> E. x ( x = y /\ x e. A ) )
8 eleq1w
 |-  ( x = y -> ( x e. A <-> y e. A ) )
9 8 equsexvw
 |-  ( E. x ( x = y /\ x e. A ) <-> y e. A )
10 7 9 bitri
 |-  ( E. x ( x e. A /\ <. x , y >. e. _I ) <-> y e. A )
11 10 abbii
 |-  { y | E. x ( x e. A /\ <. x , y >. e. _I ) } = { y | y e. A }
12 abid2
 |-  { y | y e. A } = A
13 1 11 12 3eqtri
 |-  ( _I " A ) = A