Theorem dfid3 2843

Description: A stronger version of df-id 2842 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 2842	. . 3 |- I = {<.x, z>. | x = z}
2		df-opab 2673	. . 3 |- {<.x, z>. | x = z} = {w | E.xE.z(w = <.x, z>. /\ x = z)}
3		opeq2 2493	. . . . . . . . . . 11 |- (x = y -> <.x, x>. = <.x, y>.)
4	3	eqeq2d 1489	. . . . . . . . . 10 |- (x = y -> (w = <.x, x>. <-> w = <.x, y>.))
5		equequ2 1137	. . . . . . . . . 10 |- (x = y -> (x = x <-> x = y))
6	4, 5	anbi12d 630	. . . . . . . . 9 |- (x = y -> ((w = <.x, x>. /\ x = x) <-> (w = <.x, y>. /\ x = y)))
7	6	a4s 986	. . . . . . . 8 |- (A.x x = y -> ((w = <.x, x>. /\ x = x) <-> (w = <.x, y>. /\ x = y)))
8	7	drex1 1158	. . . . . . 7 |- (A.x x = y -> (E.x(w = <.x, x>. /\ x = x) <-> E.y(w = <.x, y>. /\ x = y)))
9	8	drex2 1159	. . . . . 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 1131	. . . . . . . . . . . 12 |- (x = z <-> z = x)
12	11	anbi1i 483	. . . . . . . . . . 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 1053	. . . . . . . . 9 |- (E.z(w = <.x, z>. /\ x = z) <-> E.z(z = x /\ w = <.x, z>.))
15		visset 1816	. . . . . . . . . 10 |- x e. V
16		opeq2 2493	. . . . . . . . . . 11 |- (z = x -> <.x, z>. = <.x, x>.)
17	16	eqeq2d 1489	. . . . . . . . . 10 |- (z = x -> (w = <.x, z>. <-> w = <.x, x>.))
18	15, 17	ceqsexv 1838	. . . . . . . . 9 |- (E.z(z = x /\ w = <.x, z>.) <-> w = <.x, x>.)
19		equid 1128	. . . . . . . . . 10 |- x = x
20	19	biantru 726	. . . . . . . . 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 1053	. . . . . . 7 |- (E.xE.z(w = <.x, z>. /\ x = z) <-> E.x(w = <.x, x>. /\ x = x))
23		hbe1 1018	. . . . . . . 8 |- (E.x(w = <.x, x>. /\ x = x) -> A.xE.x(w = <.x, x>. /\ x = x))
24	23	19.9 1038	. . . . . . 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 534	. . . . 5 |- (A.x x = y -> (E.xE.z(w = <.x, z>. /\ x = z) <-> E.xE.y(w = <.x, y>. /\ x = y)))
27		hbnae 1149	. . . . . 6 |- (-. A.x x = y -> A.x -. A.x x = y)
28		hbnae 1149	. . . . . . 7 |- (-. A.x x = y -> A.y -. A.x x = y)
29		ax-17 973	. . . . . . . . . 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 1359	. . . . . . . . . . 11 |- (-. A.y y = x -> (v e. x -> A.y v e. x))
32	31	nalequcoms 1146	. . . . . . . . . 10 |- (-. A.x x = y -> (v e. x -> A.y v e. x))
33		ax-17 973	. . . . . . . . . . 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 2502	. . . . . . . . 9 |- (-. A.x x = y -> (v e. <.x, z>. -> A.y v e. <.x, z>.))
36	28, 30, 35	hbeqd 1916	. . . . . . . 8 |- (-. A.x x = y -> (w = <.x, z>. -> A.y w = <.x, z>.))
37		dveeq1 1356	. . . . . . . . 9 |- (-. A.y y = x -> (x = z -> A.y x = z))
38	37	nalequcoms 1146	. . . . . . . 8 |- (-. A.x x = y -> (x = z -> A.y x = z))
39	36, 38	hband 1113	. . . . . . 7 |- (-. A.x x = y -> ((w = <.x, z>. /\ x = z) -> A.y(w = <.x, z>. /\ x = z)))
40		opeq2 2493	. . . . . . . . . 10 |- (z = y -> <.x, z>. = <.x, y>.)
41	40	eqeq2d 1489	. . . . . . . . 9 |- (z = y -> (w = <.x, z>. <-> w = <.x, y>.))
42		equequ2 1137	. . . . . . . . 9 |- (z = y -> (x = z <-> x = y))
43	41, 42	anbi12d 630	. . . . . . . 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 1323	. . . . . 6 |- (-. A.x x = y -> (E.z(w = <.x, z>. /\ x = z) <-> E.y(w = <.x, y>. /\ x = y)))
46	27, 45	exbid 1107	. . . . 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 1578	. . 3 |- {w | E.xE.z(w = <.x, z>. /\ x = z)} = {w | E.xE.y(w = <.x, y>. /\ x = y)}
49	1, 2, 48	3eqtr 1502	. 2 |- I = {w | E.xE.y(w = <.x, y>. /\ x = y)}
50		df-opab 2673	. 2 |- {<.x, y>. | x = y} = {w | E.xE.y(w = <.x, y>. /\ x = y)}
51	49, 50	eqtr4 1501	1 |- I = {<.x, y>. | x = y}

Syntax hints:  -. wn 2   -> wi 3   <-> wb 146   /\ wa 223  A.wal 956   = wceq 958   e. wcel 960  E.wex 982  {cab 1466  <.cop 2416  {copab 2672  Icid 2838

This theorem is referenced by:  dfid2 2844

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-12 970  ax-14 972  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 983  df-sb 1174  df-clab 1467  df-cleq 1472  df-clel 1475  df-v 1815  df-un 2054  df-sn 2417  df-pr 2418  df-op 2421  df-opab 2673  df-id 2842

Copyright terms: Public domain