Theorem dfid3

Description: A stronger version of df-id that does not require x and y to be disjoint. This is not the definition since, in order to pass our definition soundness test, a definition has to have disjoint dummy variables, see conventions . The proof can be instructive in showing how disjoint variable conditions may be eliminated, a task that is not necessarily obvious. (Contributed by NM, 5-Feb-2008) (Revised by Mario Carneiro, 18-Nov-2016)

Use df-id instead to make the semantics of the constructor df-opab clearer (in usages, x , y will typically be dummy variables, so can be assumed disjoint). (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		df-id	$$⊢\mathrm{I}=\left\{⟨x,z⟩|x=z\right\}$$
2		equcom	$$⊢x=z\leftrightarrow z=x$$
3	2	anbi1ci	$$⊢\left(w=⟨x,z⟩\wedge x=z\right)\leftrightarrow \left(z=x\wedge w=⟨x,z⟩\right)$$
4	3	exbii	$$⊢\exists z\left(w=⟨x,z⟩\wedge x=z\right)\leftrightarrow \exists z\left(z=x\wedge w=⟨x,z⟩\right)$$
5		opeq2	$$⊢z=x\to ⟨x,z⟩=⟨x,x⟩$$
6	5	eqeq2d	$$⊢z=x\to \left(w=⟨x,z⟩\leftrightarrow w=⟨x,x⟩\right)$$
7	6	equsexvw	$$⊢\exists z\left(z=x\wedge w=⟨x,z⟩\right)\leftrightarrow w=⟨x,x⟩$$
8		equid	$$⊢x=x$$
9	8	biantru	$$⊢w=⟨x,x⟩\leftrightarrow \left(w=⟨x,x⟩\wedge x=x\right)$$
10	4 7 9	3bitri	$$⊢\exists z\left(w=⟨x,z⟩\wedge x=z\right)\leftrightarrow \left(w=⟨x,x⟩\wedge x=x\right)$$
11	10	exbii	$$⊢\exists x\exists z\left(w=⟨x,z⟩\wedge x=z\right)\leftrightarrow \exists x\left(w=⟨x,x⟩\wedge x=x\right)$$
12		nfe1	$$⊢Ⅎx\exists x\left(w=⟨x,x⟩\wedge x=x\right)$$
13	12	19.9	$$⊢\exists x\exists x\left(w=⟨x,x⟩\wedge x=x\right)\leftrightarrow \exists x\left(w=⟨x,x⟩\wedge x=x\right)$$
14	11 13	bitr4i	$$⊢\exists x\exists z\left(w=⟨x,z⟩\wedge x=z\right)\leftrightarrow \exists x\exists x\left(w=⟨x,x⟩\wedge x=x\right)$$
15		opeq2	$$⊢x=y\to ⟨x,x⟩=⟨x,y⟩$$
16	15	eqeq2d	$$⊢x=y\to \left(w=⟨x,x⟩\leftrightarrow w=⟨x,y⟩\right)$$
17		equequ2	$$⊢x=y\to \left(x=x\leftrightarrow x=y\right)$$
18	16 17	anbi12d	$$⊢x=y\to \left(\left(w=⟨x,x⟩\wedge x=x\right)\leftrightarrow \left(w=⟨x,y⟩\wedge x=y\right)\right)$$
19	18	sps	$$⊢\forall xx=y\to \left(\left(w=⟨x,x⟩\wedge x=x\right)\leftrightarrow \left(w=⟨x,y⟩\wedge x=y\right)\right)$$
20	19	drex1	$$⊢\forall xx=y\to \left(\exists x\left(w=⟨x,x⟩\wedge x=x\right)\leftrightarrow \exists y\left(w=⟨x,y⟩\wedge x=y\right)\right)$$
21	20	drex2	$$⊢\forall xx=y\to \left(\exists x\exists x\left(w=⟨x,x⟩\wedge x=x\right)\leftrightarrow \exists x\exists y\left(w=⟨x,y⟩\wedge x=y\right)\right)$$
22	14 21	bitrid	$$⊢\forall xx=y\to \left(\exists x\exists z\left(w=⟨x,z⟩\wedge x=z\right)\leftrightarrow \exists x\exists y\left(w=⟨x,y⟩\wedge x=y\right)\right)$$
23		nfnae	$$⊢Ⅎx\neg \forall xx=y$$
24		nfnae	$$⊢Ⅎy\neg \forall xx=y$$
25		nfcvd	$$⊢\neg \forall xx=y\to \underset{\_}{Ⅎ}yw$$
26		nfcvf2	$$⊢\neg \forall xx=y\to \underset{\_}{Ⅎ}yx$$
27		nfcvd	$$⊢\neg \forall xx=y\to \underset{\_}{Ⅎ}yz$$
28	26 27	nfopd	$$⊢\neg \forall xx=y\to \underset{\_}{Ⅎ}y⟨x,z⟩$$
29	25 28	nfeqd	$$⊢\neg \forall xx=y\to Ⅎyw=⟨x,z⟩$$
30	26 27	nfeqd	$$⊢\neg \forall xx=y\to Ⅎyx=z$$
31	29 30	nfand	$$⊢\neg \forall xx=y\to Ⅎy\left(w=⟨x,z⟩\wedge x=z\right)$$
32		opeq2	$$⊢z=y\to ⟨x,z⟩=⟨x,y⟩$$
33	32	eqeq2d	$$⊢z=y\to \left(w=⟨x,z⟩\leftrightarrow w=⟨x,y⟩\right)$$
34		equequ2	$$⊢z=y\to \left(x=z\leftrightarrow x=y\right)$$
35	33 34	anbi12d	$$⊢z=y\to \left(\left(w=⟨x,z⟩\wedge x=z\right)\leftrightarrow \left(w=⟨x,y⟩\wedge x=y\right)\right)$$
36	35	a1i	$$⊢\neg \forall xx=y\to \left(z=y\to \left(\left(w=⟨x,z⟩\wedge x=z\right)\leftrightarrow \left(w=⟨x,y⟩\wedge x=y\right)\right)\right)$$
37	24 31 36	cbvexd	$$⊢\neg \forall xx=y\to \left(\exists z\left(w=⟨x,z⟩\wedge x=z\right)\leftrightarrow \exists y\left(w=⟨x,y⟩\wedge x=y\right)\right)$$
38	23 37	exbid	$$⊢\neg \forall xx=y\to \left(\exists x\exists z\left(w=⟨x,z⟩\wedge x=z\right)\leftrightarrow \exists x\exists y\left(w=⟨x,y⟩\wedge x=y\right)\right)$$
39	22 38	pm2.61i	$$⊢\exists x\exists z\left(w=⟨x,z⟩\wedge x=z\right)\leftrightarrow \exists x\exists y\left(w=⟨x,y⟩\wedge x=y\right)$$
40	39	abbii	$$⊢\left\{w|\exists x\exists z\left(w=⟨x,z⟩\wedge x=z\right)\right\}=\left\{w|\exists x\exists y\left(w=⟨x,y⟩\wedge x=y\right)\right\}$$
41		df-opab	$$⊢\left\{⟨x,z⟩|x=z\right\}=\left\{w|\exists x\exists z\left(w=⟨x,z⟩\wedge x=z\right)\right\}$$
42		df-opab	$$⊢\left\{⟨x,y⟩|x=y\right\}=\left\{w|\exists x\exists y\left(w=⟨x,y⟩\wedge x=y\right)\right\}$$
43	40 41 42	3eqtr4i	$$⊢\left\{⟨x,z⟩|x=z\right\}=\left\{⟨x,y⟩|x=y\right\}$$
44	1 43	eqtri	$$⊢\mathrm{I}=\left\{⟨x,y⟩|x=y\right\}$$