Theorem dfid2

Description: Alternate definition of the identity relation. Instance of dfid3 not requiring auxiliary axioms. (Contributed by NM, 15-Mar-2007) Reduce axiom usage. (Revised by GG, 4-Nov-2024) (Proof shortened by BJ, 5-Nov-2024)

Use df-id instead to make the semantics of the constructor df-opab clearer. (New usage is discouraged.)

	Ref	Expression
Assertion	dfid2	$$⊢\mathrm{I}=\left\{⟨x,x⟩|x=x\right\}$$

Proof

Step	Hyp	Ref	Expression
1		df-id	$$⊢\mathrm{I}=\left\{⟨x,y⟩|x=y\right\}$$
2		equcomi	$$⊢x=y\to y=x$$
3	2	opeq2d	$$⊢x=y\to ⟨x,y⟩=⟨x,x⟩$$
4	3	eqeq2d	$$⊢x=y\to \left(z=⟨x,y⟩\leftrightarrow z=⟨x,x⟩\right)$$
5	4	pm5.32ri	$$⊢\left(z=⟨x,y⟩\wedge x=y\right)\leftrightarrow \left(z=⟨x,x⟩\wedge x=y\right)$$
6	5	exbii	$$⊢\exists y\left(z=⟨x,y⟩\wedge x=y\right)\leftrightarrow \exists y\left(z=⟨x,x⟩\wedge x=y\right)$$
7		ax6evr	$$⊢\exists yx=y$$
8		19.42v	$$⊢\exists y\left(z=⟨x,x⟩\wedge x=y\right)\leftrightarrow \left(z=⟨x,x⟩\wedge \exists yx=y\right)$$
9	7 8	mpbiran2	$$⊢\exists y\left(z=⟨x,x⟩\wedge x=y\right)\leftrightarrow z=⟨x,x⟩$$
10	6 9	bitri	$$⊢\exists y\left(z=⟨x,y⟩\wedge x=y\right)\leftrightarrow z=⟨x,x⟩$$
11		eqidd	$$⊢z=⟨x,x⟩\to x=x$$
12	11	pm4.71i	$$⊢z=⟨x,x⟩\leftrightarrow \left(z=⟨x,x⟩\wedge x=x\right)$$
13	10 12	bitri	$$⊢\exists y\left(z=⟨x,y⟩\wedge x=y\right)\leftrightarrow \left(z=⟨x,x⟩\wedge x=x\right)$$
14	13	exbii	$$⊢\exists x\exists y\left(z=⟨x,y⟩\wedge x=y\right)\leftrightarrow \exists x\left(z=⟨x,x⟩\wedge x=x\right)$$
15		id	$$⊢x=u\to x=u$$
16	15 15	opeq12d	$$⊢x=u\to ⟨x,x⟩=⟨u,u⟩$$
17	16	eqeq2d	$$⊢x=u\to \left(z=⟨x,x⟩\leftrightarrow z=⟨u,u⟩\right)$$
18	15 15	eqeq12d	$$⊢x=u\to \left(x=x\leftrightarrow u=u\right)$$
19	17 18	anbi12d	$$⊢x=u\to \left(\left(z=⟨x,x⟩\wedge x=x\right)\leftrightarrow \left(z=⟨u,u⟩\wedge u=u\right)\right)$$
20	19	exexw	$$⊢\exists x\left(z=⟨x,x⟩\wedge x=x\right)\leftrightarrow \exists x\exists x\left(z=⟨x,x⟩\wedge x=x\right)$$
21	14 20	bitri	$$⊢\exists x\exists y\left(z=⟨x,y⟩\wedge x=y\right)\leftrightarrow \exists x\exists x\left(z=⟨x,x⟩\wedge x=x\right)$$
22	21	abbii	$$⊢\left\{z|\exists x\exists y\left(z=⟨x,y⟩\wedge x=y\right)\right\}=\left\{z|\exists x\exists x\left(z=⟨x,x⟩\wedge x=x\right)\right\}$$
23		df-opab	$$⊢\left\{⟨x,y⟩|x=y\right\}=\left\{z|\exists x\exists y\left(z=⟨x,y⟩\wedge x=y\right)\right\}$$
24		df-opab	$$⊢\left\{⟨x,x⟩|x=x\right\}=\left\{z|\exists x\exists x\left(z=⟨x,x⟩\wedge x=x\right)\right\}$$
25	22 23 24	3eqtr4i	$$⊢\left\{⟨x,y⟩|x=y\right\}=\left\{⟨x,x⟩|x=x\right\}$$
26	1 25	eqtri	$$⊢\mathrm{I}=\left\{⟨x,x⟩|x=x\right\}$$