Theorem dfid3 2836

Description: A stronger version of df-id 2835 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 2835	. . 3 |- I = {<.x, z>. | x = z}
2		df-opab 2667	. . 3 |- {<.x, z>. | x = z} = {w | E.xE.z(w = <.x, z>. /\ x = z)}
3		opeq2 2488	. . . . . . . . . . 11 |- (x = y -> <.x, x>. = <.x, y>.)
4	3	eqeq2d 1486	. . . . . . . . . 10 |- (x = y -> (w = <.x, x>. <-> w = <.x, y>.))
5		equequ2 1135	. . . . . . . . . 10 |- (x = y -> (x = x <-> x = y))
6	4, 5	anbi12d 628	. . . . . . . . 9 |- (x = y -> ((w = <.x, x>. /\ x = x) <-> (w = <.x, y>. /\ x = y)))
7	6	a4s 984	. . . . . . . 8 |- (A.x x = y -> ((w = <.x, x>. /\ x = x) <-> (w = <.x, y>. /\ x = y)))
8	7	drex1 1156	. . . . . . 7 |- (A.x x = y -> (E.x(w = <.x, x>. /\ x = x) <-> E.y(w = <.x, y>. /\ x = y)))
9	8	drex2 1157	. . . . . 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 1129	. . . . . . . . . . . 12 |- (x = z <-> z = x)
12	11	anbi1i 481	. . . . . . . . . . 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 1051	. . . . . . . . 9 |- (E.z(w = <.x, z>. /\ x = z) <-> E.z(z = x /\ w = <.x, z>.))
15		visset 1813	. . . . . . . . . 10 |- x e. V
16		opeq2 2488	. . . . . . . . . . 11 |- (z = x -> <.x, z>. = <.x, x>.)
17	16	eqeq2d 1486	. . . . . . . . . 10 |- (z = x -> (w = <.x, z>. <-> w = <.x, x>.))
18	15, 17	ceqsexv 1835	. . . . . . . . 9 |- (E.z(z = x /\ w = <.x, z>.) <-> w = <.x, x>.)
19		equid 1126	. . . . . . . . . 10 |- x = x
20	19	biantru 724	. . . . . . . . 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 1051	. . . . . . 7 |- (E.xE.z(w = <.x, z>. /\ x = z) <-> E.x(w = <.x, x>. /\ x = x))
23		hbe1 1016	. . . . . . . 8 |- (E.x(w = <.x, x>. /\ x = x) -> A.xE.x(w = <.x, x>. /\ x = x))
24	23	19.9 1036	. . . . . . 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 532	. . . . 5 |- (A.x x = y -> (E.xE.z(w = <.x, z>. /\ x = z) <-> E.xE.y(w = <.x, y>. /\ x = y)))
27		hbnae 1147	. . . . . 6 |- (-. A.x x = y -> A.x -. A.x x = y)
28		hbnae 1147	. . . . . . 7 |- (-. A.x x = y -> A.y -. A.x x = y)
29		ax-17 971	. . . . . . . . . 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 1357	. . . . . . . . . . 11 |- (-. A.y y = x -> (v e. x -> A.y v e. x))
32	31	nalequcoms 1144	. . . . . . . . . 10 |- (-. A.x x = y -> (v e. x -> A.y v e. x))
33		ax-17 971	. . . . . . . . . . 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 2497	. . . . . . . . 9 |- (-. A.x x = y -> (v e. <.x, z>. -> A.y v e. <.x, z>.))
36	28, 30, 35	hbeqd 1913	. . . . . . . 8 |- (-. A.x x = y -> (w = <.x, z>. -> A.y w = <.x, z>.))
37		dveeq1 1354	. . . . . . . . 9 |- (-. A.y y = x -> (x = z -> A.y x = z))
38	37	nalequcoms 1144	. . . . . . . 8 |- (-. A.x x = y -> (x = z -> A.y x = z))
39	36, 38	hband 1111	. . . . . . 7 |- (-. A.x x = y -> ((w = <.x, z>. /\ x = z) -> A.y(w = <.x, z>. /\ x = z)))
40		opeq2 2488	. . . . . . . . . 10 |- (z = y -> <.x, z>. = <.x, y>.)
41	40	eqeq2d 1486	. . . . . . . . 9 |- (z = y -> (w = <.x, z>. <-> w = <.x, y>.))
42		equequ2 1135	. . . . . . . . 9 |- (z = y -> (x = z <-> x = y))
43	41, 42	anbi12d 628	. . . . . . . 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 1321	. . . . . 6 |- (-. A.x x = y -> (E.z(w = <.x, z>. /\ x = z) <-> E.y(w = <.x, y>. /\ x = y)))
46	27, 45	exbid 1105	. . . . 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 1575	. . 3 |- {w | E.xE.z(w = <.x, z>. /\ x = z)} = {w | E.xE.y(w = <.x, y>. /\ x = y)}
49	1, 2, 48	3eqtr 1499	. 2 |- I = {w | E.xE.y(w = <.x, y>. /\ x = y)}
50		df-opab 2667	. 2 |- {<.x, y>. | x = y} = {w | E.xE.y(w = <.x, y>. /\ x = y)}
51	49, 50	eqtr4 1498	1 |- I = {<.x, y>. | x = y}

Syntax hints:  -. wn 2   -> wi 3   <-> wb 146   /\ wa 223  A.wal 954   = wceq 956   e. wcel 958  E.wex 980  {cab 1463  <.cop 2411  {copab 2666  Icid 2831

This theorem is referenced by:  dfid2 2837

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-12 968  ax-14 970  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-v 1812  df-un 2050  df-sn 2412  df-pr 2413  df-op 2416  df-opab 2667  df-id 2835

Copyright terms: Public domain