Theorem dfid3 2799

Description: A stronger version of df-id 2797 that doesn't require x and y to be distinct. Ordinarily, we wouldn't use this as a definition, since non-distinct dummy variables would make soundness verification more difficult (as the proof here shows). The proof can be instructive in showing how distinct variable requirements may be eliminated, a task that is not necessarily obvious.

Assertion

Ref	Expression
dfid3	|- I = {<.x, y>. | x = y}

Proof of Theorem dfid3

Step	Hyp	Ref	Expression
1		df-id 2797	. . 3 |- I = {<.x, z>. | x = z}
2		df-opab 2635	. . 3 |- {<.x, z>. | x = z} = {w | E.xE.z(w = <.x, z>. /\ x = z)}
3		opeq2 2457	. . . . . . . . . . 11 |- (x = y -> <.x, x>. = <.x, y>.)
4	3	eqeq2d 1462	. . . . . . . . . 10 |- (x = y -> (w = <.x, x>. <-> w = <.x, y>.))
5		equequ2 1122	. . . . . . . . . 10 |- (x = y -> (x = x <-> x = y))
6	4, 5	anbi12d 626	. . . . . . . . 9 |- (x = y -> ((w = <.x, x>. /\ x = x) <-> (w = <.x, y>. /\ x = y)))
7	6	a4s 960	. . . . . . . 8 |- (A.x x = y -> ((w = <.x, x>. /\ x = x) <-> (w = <.x, y>. /\ x = y)))
8	7	drex1 1139	. . . . . . 7 |- (A.x x = y -> (E.x(w = <.x, x>. /\ x = x) <-> E.y(w = <.x, y>. /\ x = y)))
9	8	drex2 1140	. . . . . 6 |- (A.x x = y -> (E.xE.x(w = <.x, x>. /\ x = x) <-> E.xE.y(w = <.x, y>. /\ x = y)))
10		ancom 435	. . . . . . . . . . 11 |- ((w = <.x, z>. /\ x = z) <-> (x = z /\ w = <.x, z>.))
11		equcom 1116	. . . . . . . . . . . 12 |- (x = z <-> z = x)
12	11	anbi1i 480	. . . . . . . . . . 11 |- ((x = z /\ w = <.x, z>.) <-> (z = x /\ w = <.x, z>.))
13	10, 12	bitr 173	. . . . . . . . . 10 |- ((w = <.x, z>. /\ x = z) <-> (z = x /\ w = <.x, z>.))
14	13	exbii 1027	. . . . . . . . 9 |- (E.z(w = <.x, z>. /\ x = z) <-> E.z(z = x /\ w = <.x, z>.))
15		visset 1788	. . . . . . . . . 10 |- x e. V
16		opeq2 2457	. . . . . . . . . . 11 |- (z = x -> <.x, z>. = <.x, x>.)
17	16	eqeq2d 1462	. . . . . . . . . 10 |- (z = x -> (w = <.x, z>. <-> w = <.x, x>.))
18	15, 17	ceqsexv 1810	. . . . . . . . 9 |- (E.z(z = x /\ w = <.x, z>.) <-> w = <.x, x>.)
19		equid 1113	. . . . . . . . . 10 |- x = x
20	19	biantru 721	. . . . . . . . 9 |- (w = <.x, x>. <-> (w = <.x, x>. /\ x = x))
21	14, 18, 20	3bitr 177	. . . . . . . 8 |- (E.z(w = <.x, z>. /\ x = z) <-> (w = <.x, x>. /\ x = x))
22	21	exbii 1027	. . . . . . 7 |- (E.xE.z(w = <.x, z>. /\ x = z) <-> E.x(w = <.x, x>. /\ x = x))
23		hbe1 990	. . . . . . . 8 |- (E.x(w = <.x, x>. /\ x = x) -> A.xE.x(w = <.x, x>. /\ x = x))
24	23	19.9 1012	. . . . . . 7 |- (E.xE.x(w = <.x, x>. /\ x = x) <-> E.x(w = <.x, x>. /\ x = x))
25	22, 24	bitr4 176	. . . . . 6 |- (E.xE.z(w = <.x, z>. /\ x = z) <-> E.xE.x(w = <.x, x>. /\ x = x))
26	9, 25	syl5bb 530	. . . . 5 |- (A.x x = y -> (E.xE.z(w = <.x, z>. /\ x = z) <-> E.xE.y(w = <.x, y>. /\ x = y)))
27		hbnae 1130	. . . . . 6 |- (-. A.x x = y -> A.x -. A.x x = y)
28		hbnae 1130	. . . . . . 7 |- (-. A.x x = y -> A.y -. A.x x = y)
29		ax-17 1190	. . . . . . . . . 10 |- (v e. w -> A.y v e. w)
30	29	a1i 8	. . . . . . . . 9 |- (-. A.x x = y -> (v e. w -> A.y v e. w))
31		dveel2 1337	. . . . . . . . . . 11 |- (-. A.y y = x -> (v e. x -> A.y v e. x))
32	31	nalequcoms 1127	. . . . . . . . . 10 |- (-. A.x x = y -> (v e. x -> A.y v e. x))
33		ax-17 1190	. . . . . . . . . . 11 |- (v e. z -> A.y v e. z)
34	33	a1i 8	. . . . . . . . . 10 |- (-. A.x x = y -> (v e. z -> A.y v e. z))
35	28, 32, 34	hbopd 2466	. . . . . . . . 9 |- (-. A.x x = y -> (v e. <.x, z>. -> A.y v e. <.x, z>.))
36	28, 30, 35	hbeqd 1885	. . . . . . . 8 |- (-. A.x x = y -> (w = <.x, z>. -> A.y w = <.x, z>.))
37		dveeq1 1335	. . . . . . . . 9 |- (-. A.y y = x -> (x = z -> A.y x = z))
38	37	nalequcoms 1127	. . . . . . . 8 |- (-. A.x x = y -> (x = z -> A.y x = z))
39	36, 38	hband 1087	. . . . . . 7 |- (-. A.x x = y -> ((w = <.x, z>. /\ x = z) -> A.y(w = <.x, z>. /\ x = z)))
40		opeq2 2457	. . . . . . . . . 10 |- (z = y -> <.x, z>. = <.x, y>.)
41	40	eqeq2d 1462	. . . . . . . . 9 |- (z = y -> (w = <.x, z>. <-> w = <.x, y>.))
42		equequ2 1122	. . . . . . . . 9 |- (z = y -> (x = z <-> x = y))
43	41, 42	anbi12d 626	. . . . . . . 8 |- (z = y -> ((w = <.x, z>. /\ x = z) <-> (w = <.x, y>. /\ x = y)))
44	43	a1i 8	. . . . . . 7 |- (-. A.x x = y -> (z = y -> ((w = <.x, z>. /\ x = z) <-> (w = <.x, y>. /\ x = y))))
45	28, 39, 44	cbvexd 1303	. . . . . 6 |- (-. A.x x = y -> (E.z(w = <.x, z>. /\ x = z) <-> E.y(w = <.x, y>. /\ x = y)))
46	27, 45	exbid 1081	. . . . 5 |- (-. A.x x = y -> (E.xE.z(w = <.x, z>. /\ x = z) <-> E.xE.y(w = <.x, y>. /\ x = y)))
47	26, 46	pm2.61i 126	. . . 4 |- (E.xE.z(w = <.x, z>. /\ x = z) <-> E.xE.y(w = <.x, y>. /\ x = y))
48	47	abbii 1551	. . 3 |- {w | E.xE.z(w = <.x, z>. /\ x = z)} = {w | E.xE.y(w = <.x, y>. /\ x = y)}
49	1, 2, 48	3eqtr 1475	. 2 |- I = {w | E.xE.y(w = <.x, y>. /\ x = y)}
50		df-opab 2635	. 2 |- {<.x, y>. | x = y} = {w | E.xE.y(w = <.x, y>. /\ x = y)}
51	49, 50	eqtr4 1474	1 |- I = {<.x, y>. | x = y}

Syntax hints:  -. wn 2   -> wi 3   <-> wb 146   /\ wa 223  A.wal 950  E.wex 956   = wceq 1099   e. wcel 1105  {cab 1440  <.cop 2382  {copab 2634  Icid 2793

This theorem is referenced by:  dfid2 2800

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-4 951  ax-5 952  ax-6 953  ax-7 954  ax-gen 955  ax-8 1101  ax-9 1102  ax-10 1103  ax-12 1104  ax-14 1108  ax-17 1190  ax-16 1194  ax-11o 1202  ax-ext 1436

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 957  df-sb 1155  df-clab 1441  df-cleq 1446  df-clel 1449  df-v 1787  df-un 2021  df-sn 2383  df-pr 2384  df-op 2387  df-opab 2635  df-id 2797

Copyright terms: Public domain