Description: The converse of the identity relation. Theorem 3.7(ii) of Monk1 p. 36. (Contributed by NM, 26-Apr-1998) (Proof shortened by Andrew Salmon, 27-Aug-2011)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | cnvi | |- `' _I = _I |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | vex | |- x e. _V |
|
| 2 | 1 | ideq | |- ( y _I x <-> y = x ) |
| 3 | equcom | |- ( y = x <-> x = y ) |
|
| 4 | 2 3 | bitri | |- ( y _I x <-> x = y ) |
| 5 | 4 | opabbii | |- { <. x , y >. | y _I x } = { <. x , y >. | x = y } |
| 6 | df-cnv | |- `' _I = { <. x , y >. | y _I x } |
|
| 7 | df-id | |- _I = { <. x , y >. | x = y } |
|
| 8 | 5 6 7 | 3eqtr4i | |- `' _I = _I |