Theorem dfid3 2831

Description: A stronger version of df-id 2830 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 2830	. . 3 |- I = {<.x, z>. | x = z}
2		df-opab 2662	. . 3 |- {<.x, z>. | x = z} = {w | E.xE.z(w = <.x, z>. /\ x = z)}
3		opeq2 2484	. . . . . . . . . . 11 |- (x = y -> <.x, x>. = <.x, y>.)
4	3	eqeq2d 1483	. . . . . . . . . 10 |- (x = y -> (w = <.x, x>. <-> w = <.x, y>.))
5		equequ2 1133	. . . . . . . . . 10 |- (x = y -> (x = x <-> x = y))
6	4, 5	anbi12d 627	. . . . . . . . 9 |- (x = y -> ((w = <.x, x>. /\ x = x) <-> (w = <.x, y>. /\ x = y)))
7	6	a4s 982	. . . . . . . 8 |- (A.x x = y -> ((w = <.x, x>. /\ x = x) <-> (w = <.x, y>. /\ x = y)))
8	7	drex1 1154	. . . . . . 7 |- (A.x x = y -> (E.x(w = <.x, x>. /\ x = x) <-> E.y(w = <.x, y>. /\ x = y)))
9	8	drex2 1155	. . . . . 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 1127	. . . . . . . . . . . 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 1049	. . . . . . . . 9 |- (E.z(w = <.x, z>. /\ x = z) <-> E.z(z = x /\ w = <.x, z>.))
15		visset 1809	. . . . . . . . . 10 |- x e. V
16		opeq2 2484	. . . . . . . . . . 11 |- (z = x -> <.x, z>. = <.x, x>.)
17	16	eqeq2d 1483	. . . . . . . . . 10 |- (z = x -> (w = <.x, z>. <-> w = <.x, x>.))
18	15, 17	ceqsexv 1831	. . . . . . . . 9 |- (E.z(z = x /\ w = <.x, z>.) <-> w = <.x, x>.)
19		equid 1124	. . . . . . . . . 10 |- x = x
20	19	biantru 723	. . . . . . . . 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 1049	. . . . . . 7 |- (E.xE.z(w = <.x, z>. /\ x = z) <-> E.x(w = <.x, x>. /\ x = x))
23		hbe1 1014	. . . . . . . 8 |- (E.x(w = <.x, x>. /\ x = x) -> A.xE.x(w = <.x, x>. /\ x = x))
24	23	19.9 1034	. . . . . . 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 531	. . . . 5 |- (A.x x = y -> (E.xE.z(w = <.x, z>. /\ x = z) <-> E.xE.y(w = <.x, y>. /\ x = y)))
27		hbnae 1145	. . . . . 6 |- (-. A.x x = y -> A.x -. A.x x = y)
28		hbnae 1145	. . . . . . 7 |- (-. A.x x = y -> A.y -. A.x x = y)
29		ax-17 969	. . . . . . . . . 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 1355	. . . . . . . . . . 11 |- (-. A.y y = x -> (v e. x -> A.y v e. x))
32	31	nalequcoms 1142	. . . . . . . . . 10 |- (-. A.x x = y -> (v e. x -> A.y v e. x))
33		ax-17 969	. . . . . . . . . . 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 2493	. . . . . . . . 9 |- (-. A.x x = y -> (v e. <.x, z>. -> A.y v e. <.x, z>.))
36	28, 30, 35	hbeqd 1909	. . . . . . . 8 |- (-. A.x x = y -> (w = <.x, z>. -> A.y w = <.x, z>.))
37		dveeq1 1352	. . . . . . . . 9 |- (-. A.y y = x -> (x = z -> A.y x = z))
38	37	nalequcoms 1142	. . . . . . . 8 |- (-. A.x x = y -> (x = z -> A.y x = z))
39	36, 38	hband 1109	. . . . . . 7 |- (-. A.x x = y -> ((w = <.x, z>. /\ x = z) -> A.y(w = <.x, z>. /\ x = z)))
40		opeq2 2484	. . . . . . . . . 10 |- (z = y -> <.x, z>. = <.x, y>.)
41	40	eqeq2d 1483	. . . . . . . . 9 |- (z = y -> (w = <.x, z>. <-> w = <.x, y>.))
42		equequ2 1133	. . . . . . . . 9 |- (z = y -> (x = z <-> x = y))
43	41, 42	anbi12d 627	. . . . . . . 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 1319	. . . . . 6 |- (-. A.x x = y -> (E.z(w = <.x, z>. /\ x = z) <-> E.y(w = <.x, y>. /\ x = y)))
46	27, 45	exbid 1103	. . . . 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 1572	. . 3 |- {w | E.xE.z(w = <.x, z>. /\ x = z)} = {w | E.xE.y(w = <.x, y>. /\ x = y)}
49	1, 2, 48	3eqtr 1496	. 2 |- I = {w | E.xE.y(w = <.x, y>. /\ x = y)}
50		df-opab 2662	. 2 |- {<.x, y>. | x = y} = {w | E.xE.y(w = <.x, y>. /\ x = y)}
51	49, 50	eqtr4 1495	1 |- I = {<.x, y>. | x = y}

Syntax hints:  -. wn 2   -> wi 3   <-> wb 146   /\ wa 223  A.wal 952   = wceq 954   e. wcel 956  E.wex 978  {cab 1461  <.cop 2407  {copab 2661  Icid 2826

This theorem is referenced by:  dfid2 2832

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-12 966  ax-14 968  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 979  df-sb 1170  df-clab 1462  df-cleq 1467  df-clel 1470  df-v 1808  df-un 2046  df-sn 2408  df-pr 2409  df-op 2412  df-opab 2662  df-id 2830

Copyright terms: Public domain