This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 = 𝑦 }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cid	⊢ I
1		vx	⊢ 𝑥
2		vy	⊢ 𝑦
3	1	cv	⊢ 𝑥
4	2	cv	⊢ 𝑦
5	3 4	wceq	⊢ 𝑥 = 𝑦
6	5 1 2	copab	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 = 𝑦 }
7	0 6	wceq	⊢ I = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 = 𝑦 }