Theorem dfid3 2832

Description: A stronger version of df-id 2831 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 2831	. . 3 ⊢ I = {⟨x, z⟩∣x = z}
2		df-opab 2663	. . 3 ⊢ {⟨x, z⟩∣x = z} = {w∣∃x∃z(w = ⟨x, z⟩ ⋀ x = z)}
3		opeq2 2485	. . . . . . . . . . 11 ⊢ (x = y → ⟨x, x⟩ = ⟨x, y⟩)
4	3	eqeq2d 1484	. . . . . . . . . 10 ⊢ (x = y → (w = ⟨x, x⟩ ↔ w = ⟨x, y⟩))
5		equequ2 1134	. . . . . . . . . 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 983	. . . . . . . 8 ⊢ (∀x x = y → ((w = ⟨x, x⟩ ⋀ x = x) ↔ (w = ⟨x, y⟩ ⋀ x = y)))
8	7	drex1 1155	. . . . . . 7 ⊢ (∀x x = y → (∃x(w = ⟨x, x⟩ ⋀ x = x) ↔ ∃y(w = ⟨x, y⟩ ⋀ x = y)))
9	8	drex2 1156	. . . . . 6 ⊢ (∀x x = y → (∃x∃x(w = ⟨x, x⟩ ⋀ x = x) ↔ ∃x∃y(w = ⟨x, y⟩ ⋀ x = y)))
10		ancom 435	. . . . . . . . . . 11 ⊢ ((w = ⟨x, z⟩ ⋀ x = z) ↔ (x = z ⋀ w = ⟨x, z⟩))
11		equcom 1128	. . . . . . . . . . . 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 1050	. . . . . . . . 9 ⊢ (∃z(w = ⟨x, z⟩ ⋀ x = z) ↔ ∃z(z = x ⋀ w = ⟨x, z⟩))
15		visset 1810	. . . . . . . . . 10 ⊢ x ∈ V
16		opeq2 2485	. . . . . . . . . . 11 ⊢ (z = x → ⟨x, z⟩ = ⟨x, x⟩)
17	16	eqeq2d 1484	. . . . . . . . . 10 ⊢ (z = x → (w = ⟨x, z⟩ ↔ w = ⟨x, x⟩))
18	15, 17	ceqsexv 1832	. . . . . . . . 9 ⊢ (∃z(z = x ⋀ w = ⟨x, z⟩) ↔ w = ⟨x, x⟩)
19		equid 1125	. . . . . . . . . 10 ⊢ x = x
20	19	biantru 723	. . . . . . . . 9 ⊢ (w = ⟨x, x⟩ ↔ (w = ⟨x, x⟩ ⋀ x = x))
21	14, 18, 20	3bitr 177	. . . . . . . 8 ⊢ (∃z(w = ⟨x, z⟩ ⋀ x = z) ↔ (w = ⟨x, x⟩ ⋀ x = x))
22	21	exbii 1050	. . . . . . 7 ⊢ (∃x∃z(w = ⟨x, z⟩ ⋀ x = z) ↔ ∃x(w = ⟨x, x⟩ ⋀ x = x))
23		hbe1 1015	. . . . . . . 8 ⊢ (∃x(w = ⟨x, x⟩ ⋀ x = x) → ∀x∃x(w = ⟨x, x⟩ ⋀ x = x))
24	23	19.9 1035	. . . . . . 7 ⊢ (∃x∃x(w = ⟨x, x⟩ ⋀ x = x) ↔ ∃x(w = ⟨x, x⟩ ⋀ x = x))
25	22, 24	bitr4 176	. . . . . 6 ⊢ (∃x∃z(w = ⟨x, z⟩ ⋀ x = z) ↔ ∃x∃x(w = ⟨x, x⟩ ⋀ x = x))
26	9, 25	syl5bb 531	. . . . 5 ⊢ (∀x x = y → (∃x∃z(w = ⟨x, z⟩ ⋀ x = z) ↔ ∃x∃y(w = ⟨x, y⟩ ⋀ x = y)))
27		hbnae 1146	. . . . . 6 ⊢ (¬ ∀x x = y → ∀x ¬ ∀x x = y)
28		hbnae 1146	. . . . . . 7 ⊢ (¬ ∀x x = y → ∀y ¬ ∀x x = y)
29		ax-17 970	. . . . . . . . . 10 ⊢ (v ∈ w → ∀y v ∈ w)
30	29	a1i 8	. . . . . . . . 9 ⊢ (¬ ∀x x = y → (v ∈ w → ∀y v ∈ w))
31		dveel2 1356	. . . . . . . . . . 11 ⊢ (¬ ∀y y = x → (v ∈ x → ∀y v ∈ x))
32	31	nalequcoms 1143	. . . . . . . . . 10 ⊢ (¬ ∀x x = y → (v ∈ x → ∀y v ∈ x))
33		ax-17 970	. . . . . . . . . . 11 ⊢ (v ∈ z → ∀y v ∈ z)
34	33	a1i 8	. . . . . . . . . 10 ⊢ (¬ ∀x x = y → (v ∈ z → ∀y v ∈ z))
35	28, 32, 34	hbopd 2494	. . . . . . . . 9 ⊢ (¬ ∀x x = y → (v ∈ ⟨x, z⟩ → ∀y v ∈ ⟨x, z⟩))
36	28, 30, 35	hbeqd 1910	. . . . . . . 8 ⊢ (¬ ∀x x = y → (w = ⟨x, z⟩ → ∀y w = ⟨x, z⟩))
37		dveeq1 1353	. . . . . . . . 9 ⊢ (¬ ∀y y = x → (x = z → ∀y x = z))
38	37	nalequcoms 1143	. . . . . . . 8 ⊢ (¬ ∀x x = y → (x = z → ∀y x = z))
39	36, 38	hband 1110	. . . . . . 7 ⊢ (¬ ∀x x = y → ((w = ⟨x, z⟩ ⋀ x = z) → ∀y(w = ⟨x, z⟩ ⋀ x = z)))
40		opeq2 2485	. . . . . . . . . 10 ⊢ (z = y → ⟨x, z⟩ = ⟨x, y⟩)
41	40	eqeq2d 1484	. . . . . . . . 9 ⊢ (z = y → (w = ⟨x, z⟩ ↔ w = ⟨x, y⟩))
42		equequ2 1134	. . . . . . . . 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 ⊢ (¬ ∀x x = y → (z = y → ((w = ⟨x, z⟩ ⋀ x = z) ↔ (w = ⟨x, y⟩ ⋀ x = y))))
45	28, 39, 44	cbvexd 1320	. . . . . 6 ⊢ (¬ ∀x x = y → (∃z(w = ⟨x, z⟩ ⋀ x = z) ↔ ∃y(w = ⟨x, y⟩ ⋀ x = y)))
46	27, 45	exbid 1104	. . . . 5 ⊢ (¬ ∀x x = y → (∃x∃z(w = ⟨x, z⟩ ⋀ x = z) ↔ ∃x∃y(w = ⟨x, y⟩ ⋀ x = y)))
47	26, 46	pm2.61i 126	. . . 4 ⊢ (∃x∃z(w = ⟨x, z⟩ ⋀ x = z) ↔ ∃x∃y(w = ⟨x, y⟩ ⋀ x = y))
48	47	abbii 1573	. . 3 ⊢ {w∣∃x∃z(w = ⟨x, z⟩ ⋀ x = z)} = {w∣∃x∃y(w = ⟨x, y⟩ ⋀ x = y)}
49	1, 2, 48	3eqtr 1497	. 2 ⊢ I = {w∣∃x∃y(w = ⟨x, y⟩ ⋀ x = y)}
50		df-opab 2663	. 2 ⊢ {⟨x, y⟩∣x = y} = {w∣∃x∃y(w = ⟨x, y⟩ ⋀ x = y)}
51	49, 50	eqtr4 1496	1 ⊢ I = {⟨x, y⟩∣x = y}

Syntax hints:  ¬ wn 2   → wi 3   ↔ wb 146   ⋀ wa 223  ∀wal 953   = wceq 955   ∈ wcel 957  ∃wex 979  {cab 1462  ⟨cop 2408  {copab 2662  Icid 2827

This theorem is referenced by:  dfid2 2833

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 961  ax-gen 962  ax-8 963  ax-10 965  ax-12 967  ax-14 969  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-10o 1139  ax-16 1209  ax-11o 1217  ax-ext 1458

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 980  df-sb 1171  df-clab 1463  df-cleq 1468  df-clel 1471  df-v 1809  df-un 2047  df-sn 2409  df-pr 2410  df-op 2413  df-opab 2663  df-id 2831

Copyright terms: Public domain