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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cid	$$class\mathrm{I}$$
1		vx	$$setvarx$$
2		vy	$$setvary$$
3	1	cv	$$setvarx$$
4	2	cv	$$setvary$$
5	3 4	wceq	$$wffx=y$$
6	5 1 2	copab	$$class\left\{⟨x,y⟩|x=y\right\}$$
7	0 6	wceq	$$wff\mathrm{I}=\left\{⟨x,y⟩|x=y\right\}$$