Theorem dfid3 2914

Description: A stronger version of df-id 2913 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 2913	. . 3 |- I = {<.x, z>. | x = z}
2		df-opab 2741	. . 3 |- {<.x, z>. | x = z} = {w | E.xE.z(w = <.x, z>. /\ x = z)}
3		opeq2 2553	. . . . . . . . . . 11 |- (x = y -> <.x, x>. = <.x, y>.)
4	3	eqeq2d 1529	. . . . . . . . . 10 |- (x = y -> (w = <.x, x>. <-> w = <.x, y>.))
5		equequ2 1172	. . . . . . . . . 10 |- (x = y -> (x = x <-> x = y))
6	4, 5	anbi12d 631	. . . . . . . . 9 |- (x = y -> ((w = <.x, x>. /\ x = x) <-> (w = <.x, y>. /\ x = y)))
7	6	a4s 1020	. . . . . . . 8 |- (A.x x = y -> ((w = <.x, x>. /\ x = x) <-> (w = <.x, y>. /\ x = y)))
8	7	drex1 1193	. . . . . . 7 |- (A.x x = y -> (E.x(w = <.x, x>. /\ x = x) <-> E.y(w = <.x, y>. /\ x = y)))
9	8	drex2 1194	. . . . . 6 |- (A.x x = y -> (E.xE.x(w = <.x, x>. /\ x = x) <-> E.xE.y(w = <.x, y>. /\ x = y)))
10		ancom 437	. . . . . . . . . . 11 |- ((w = <.x, z>. /\ x = z) <-> (x = z /\ w = <.x, z>.))
11		equcom 1166	. . . . . . . . . . . 12 |- (x = z <-> z = x)
12	11	anbi1i 484	. . . . . . . . . . 11 |- ((x = z /\ w = <.x, z>.) <-> (z = x /\ w = <.x, z>.))
13	10, 12	bitri 171	. . . . . . . . . 10 |- ((w = <.x, z>. /\ x = z) <-> (z = x /\ w = <.x, z>.))
14	13	exbii 1087	. . . . . . . . 9 |- (E.z(w = <.x, z>. /\ x = z) <-> E.z(z = x /\ w = <.x, z>.))
15		visset 1859	. . . . . . . . . 10 |- x e. V
16		opeq2 2553	. . . . . . . . . . 11 |- (z = x -> <.x, z>. = <.x, x>.)
17	16	eqeq2d 1529	. . . . . . . . . 10 |- (z = x -> (w = <.x, z>. <-> w = <.x, x>.))
18	15, 17	ceqsexv 1881	. . . . . . . . 9 |- (E.z(z = x /\ w = <.x, z>.) <-> w = <.x, x>.)
19		equid 1162	. . . . . . . . . 10 |- x = x
20	19	biantru 729	. . . . . . . . 9 |- (w = <.x, x>. <-> (w = <.x, x>. /\ x = x))
21	14, 18, 20	3bitri 175	. . . . . . . 8 |- (E.z(w = <.x, z>. /\ x = z) <-> (w = <.x, x>. /\ x = x))
22	21	exbii 1087	. . . . . . 7 |- (E.xE.z(w = <.x, z>. /\ x = z) <-> E.x(w = <.x, x>. /\ x = x))
23		hbe1 1052	. . . . . . . 8 |- (E.x(w = <.x, x>. /\ x = x) -> A.xE.x(w = <.x, x>. /\ x = x))
24	23	19.9 1072	. . . . . . 7 |- (E.xE.x(w = <.x, x>. /\ x = x) <-> E.x(w = <.x, x>. /\ x = x))
25	22, 24	bitr4i 174	. . . . . 6 |- (E.xE.z(w = <.x, z>. /\ x = z) <-> E.xE.x(w = <.x, x>. /\ x = x))
26	9, 25	syl5bb 535	. . . . 5 |- (A.x x = y -> (E.xE.z(w = <.x, z>. /\ x = z) <-> E.xE.y(w = <.x, y>. /\ x = y)))
27		hbnae 1184	. . . . . 6 |- (-. A.x x = y -> A.x -. A.x x = y)
28		hbnae 1184	. . . . . . 7 |- (-. A.x x = y -> A.y -. A.x x = y)
29		ax-17 1007	. . . . . . . . . 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 1396	. . . . . . . . . . 11 |- (-. A.y y = x -> (v e. x -> A.y v e. x))
32	31	nalequcoms 1181	. . . . . . . . . 10 |- (-. A.x x = y -> (v e. x -> A.y v e. x))
33		ax-17 1007	. . . . . . . . . . 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 2562	. . . . . . . . 9 |- (-. A.x x = y -> (v e. <.x, z>. -> A.y v e. <.x, z>.))
36	28, 30, 35	hbeqd 1959	. . . . . . . 8 |- (-. A.x x = y -> (w = <.x, z>. -> A.y w = <.x, z>.))
37		dveeq1 1393	. . . . . . . . 9 |- (-. A.y y = x -> (x = z -> A.y x = z))
38	37	nalequcoms 1181	. . . . . . . 8 |- (-. A.x x = y -> (x = z -> A.y x = z))
39	36, 38	hband 1147	. . . . . . 7 |- (-. A.x x = y -> ((w = <.x, z>. /\ x = z) -> A.y(w = <.x, z>. /\ x = z)))
40		opeq2 2553	. . . . . . . . . 10 |- (z = y -> <.x, z>. = <.x, y>.)
41	40	eqeq2d 1529	. . . . . . . . 9 |- (z = y -> (w = <.x, z>. <-> w = <.x, y>.))
42		equequ2 1172	. . . . . . . . 9 |- (z = y -> (x = z <-> x = y))
43	41, 42	anbi12d 631	. . . . . . . 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 1359	. . . . . 6 |- (-. A.x x = y -> (E.z(w = <.x, z>. /\ x = z) <-> E.y(w = <.x, y>. /\ x = y)))
46	27, 45	exbid 1141	. . . . 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 124	. . . 4 |- (E.xE.z(w = <.x, z>. /\ x = z) <-> E.xE.y(w = <.x, y>. /\ x = y))
48	47	abbii 1618	. . 3 |- {w | E.xE.z(w = <.x, z>. /\ x = z)} = {w | E.xE.y(w = <.x, y>. /\ x = y)}
49	1, 2, 48	3eqtri 1542	. 2 |- I = {w | E.xE.y(w = <.x, y>. /\ x = y)}
50		df-opab 2741	. 2 |- {<.x, y>. | x = y} = {w | E.xE.y(w = <.x, y>. /\ x = y)}
51	49, 50	eqtr4i 1541	1 |- I = {<.x, y>. | x = y}

Syntax hints:  -. wn 2   -> wi 3   <-> wb 144   /\ wa 221  A.wal 990   = wceq 992   e. wcel 994  E.wex 1016  {cab 1505  <.cop 2469  {copab 2740  Icid 2909

This theorem is referenced by:  dfid2 2915

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-10 1002  ax-12 1004  ax-14 1006  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255  ax-ext 1500

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-ex 1017  df-sb 1209  df-clab 1506  df-cleq 1511  df-clel 1514  df-v 1858  df-un 2102  df-sn 2470  df-pr 2471  df-op 2474  df-opab 2741  df-id 2913

Copyright terms: Public domain