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 | x x A x y I
2 df-br x I y x y I
3 vex y V
4 3 ideq x I y x = y
5 2 4 bitr3i x y I x = y
6 5 anbi1ci x A x y I x = y x A
7 6 exbii x x A x y I x x = y x A
8 eleq1w x = y x A y A
9 8 equsexvw x x = y x A y A
10 7 9 bitri x x A x y I y A
11 10 abbii y | x x A x y I = y | y A
12 abid2 y | y A = A
13 1 11 12 3eqtri I A = A