Theorem bj-dfid2ALT

Description: Alternate version of dfid2 . (Contributed by BJ, 9-Nov-2024) (Proof modification is discouraged.) Use df-id instead to make the semantics of the construction df-opab clearer. (New usage is discouraged.)

	Ref	Expression
Assertion	bj-dfid2ALT	$$⊢\mathrm{I}=\left\{⟨x,x⟩|\top \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	10	exbii	$$⊢\exists x\exists y\left(z=⟨x,y⟩\wedge x=y\right)\leftrightarrow \exists xz=⟨x,x⟩$$
12		id	$$⊢x=u\to x=u$$
13	12 12	opeq12d	$$⊢x=u\to ⟨x,x⟩=⟨u,u⟩$$
14	13	eqeq2d	$$⊢x=u\to \left(z=⟨x,x⟩\leftrightarrow z=⟨u,u⟩\right)$$
15	14	exexw	$$⊢\exists xz=⟨x,x⟩\leftrightarrow \exists x\exists xz=⟨x,x⟩$$
16	11 15	bitri	$$⊢\exists x\exists y\left(z=⟨x,y⟩\wedge x=y\right)\leftrightarrow \exists x\exists xz=⟨x,x⟩$$
17		tru	$$⊢\top$$
18	17	biantru	$$⊢z=⟨x,x⟩\leftrightarrow \left(z=⟨x,x⟩\wedge \top \right)$$
19	18	exbii	$$⊢\exists xz=⟨x,x⟩\leftrightarrow \exists x\left(z=⟨x,x⟩\wedge \top \right)$$
20	19	exbii	$$⊢\exists x\exists xz=⟨x,x⟩\leftrightarrow \exists x\exists x\left(z=⟨x,x⟩\wedge \top \right)$$
21	16 20	bitri	$$⊢\exists x\exists y\left(z=⟨x,y⟩\wedge x=y\right)\leftrightarrow \exists x\exists x\left(z=⟨x,x⟩\wedge \top \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 \top \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⟩|\top \right\}=\left\{z|\exists x\exists x\left(z=⟨x,x⟩\wedge \top \right)\right\}$$
25	22 23 24	3eqtr4i	$$⊢\left\{⟨x,y⟩|x=y\right\}=\left\{⟨x,x⟩|\top \right\}$$
26	1 25	eqtri	$$⊢\mathrm{I}=\left\{⟨x,x⟩|\top \right\}$$