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	$$⊢\mathrm{I}=\left\{⟨x,x⟩|x=x\right\}$$

Proof

Step	Hyp	Ref	Expression
1		dfid3	$$⊢\mathrm{I}=\left\{⟨x,x⟩|x=x\right\}$$