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