Metamath Proof Explorer


Theorem cnvi

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

Proof

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