Metamath Proof Explorer

Definition df-id

Description: Define the identity relation. Definition 9.15 of Quine p. 64. For example, 5I 5 and -. 4 I 5 ( ex-id ). (Contributed by NM, 13-Aug-1995)

Ref Expression
Assertion df-id 
|- _I = { <. x , y >. | x = y }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cid 
 |-  _I
1 vx 
 |-  x
2 vy 
 |-  y
3 1 cv 
 |-  x
4 2 cv 
 |-  y
5 3 4 wceq 
 |-  x = y
6 5 1 2 copab 
 |-  { <. x , y >. | x = y }
7 0 6 wceq 
 |-  _I = { <. x , y >. | x = y }