Theorem dfid2

Description: Alternate definition of the identity relation. (Contributed by NM, 15-Mar-2007) Use df-id when sufficient (see comment at dfid3 ). (New usage is discouraged.)

	Ref	Expression
Assertion	dfid2	|- _I = { <. x , x >. | x = x }

Proof

Step	Hyp	Ref	Expression
1		dfid3	|- _I = { <. x , x >. | x = x }