Theorem dtruALT 2744

Description: A version of dtru 2768 ("two things exist") proved directly from the axioms (no set theory definitions).

Assertion

Ref	Expression
dtruALT	⊢ ¬ ∀x x = y

Distinct variable group:   x,y

Proof of Theorem dtruALT

Step	Hyp	Ref	Expression
1		eeanv 1322	. . . . 5 ⊢ (∃w∃z(x ∈ w ⋀ ¬ x ∈ z) ↔ (∃w x ∈ w ⋀ ∃z ¬ x ∈ z))
2		ax-pow 2738	. . . . . 6 ⊢ ∃w∀z(∀y(y ∈ z → y ∈ x) → z ∈ w)
3		id 59	. . . . . . . . 9 ⊢ (y ∈ x → y ∈ x)
4	3	ax-gen 962	. . . . . . . 8 ⊢ ∀y(y ∈ x → y ∈ x)
5		elequ2 1136	. . . . . . . . . . . 12 ⊢ (z = x → (y ∈ z ↔ y ∈ x))
6	5	imbi1d 612	. . . . . . . . . . 11 ⊢ (z = x → ((y ∈ z → y ∈ x) ↔ (y ∈ x → y ∈ x)))
7	6	albidv 1277	. . . . . . . . . 10 ⊢ (z = x → (∀y(y ∈ z → y ∈ x) ↔ ∀y(y ∈ x → y ∈ x)))
8		elequ1 1135	. . . . . . . . . 10 ⊢ (z = x → (z ∈ w ↔ x ∈ w))
9	7, 8	imbi12d 625	. . . . . . . . 9 ⊢ (z = x → ((∀y(y ∈ z → y ∈ x) → z ∈ w) ↔ (∀y(y ∈ x → y ∈ x) → x ∈ w)))
10	9	a4v 1271	. . . . . . . 8 ⊢ (∀z(∀y(y ∈ z → y ∈ x) → z ∈ w) → (∀y(y ∈ x → y ∈ x) → x ∈ w))
11	4, 10	mpi 44	. . . . . . 7 ⊢ (∀z(∀y(y ∈ z → y ∈ x) → z ∈ w) → x ∈ w)
12	11	19.22i 1039	. . . . . 6 ⊢ (∃w∀z(∀y(y ∈ z → y ∈ x) → z ∈ w) → ∃w x ∈ w)
13	2, 12	ax-mp 7	. . . . 5 ⊢ ∃w x ∈ w
14		ax-nul 2706	. . . . . 6 ⊢ ∃z∀x ¬ x ∈ z
15		ax-4 972	. . . . . . 7 ⊢ (∀x ¬ x ∈ z → ¬ x ∈ z)
16	15	19.22i 1039	. . . . . 6 ⊢ (∃z∀x ¬ x ∈ z → ∃z ¬ x ∈ z)
17	14, 16	ax-mp 7	. . . . 5 ⊢ ∃z ¬ x ∈ z
18	1, 13, 17	mpbir2an 729	. . . 4 ⊢ ∃w∃z(x ∈ w ⋀ ¬ x ∈ z)
19		ax-14 969	. . . . . . . 8 ⊢ (w = z → (x ∈ w → x ∈ z))
20	19	com12 11	. . . . . . 7 ⊢ (x ∈ w → (w = z → x ∈ z))
21	20	con3d 95	. . . . . 6 ⊢ (x ∈ w → (¬ x ∈ z → ¬ w = z))
22	21	imp 350	. . . . 5 ⊢ ((x ∈ w ⋀ ¬ x ∈ z) → ¬ w = z)
23	22	19.22i2 1040	. . . 4 ⊢ (∃w∃z(x ∈ w ⋀ ¬ x ∈ z) → ∃w∃z ¬ w = z)
24	18, 23	ax-mp 7	. . 3 ⊢ ∃w∃z ¬ w = z
25		equequ2 1134	. . . . . . 7 ⊢ (z = y → (w = z ↔ w = y))
26	25	negbid 610	. . . . . 6 ⊢ (z = y → (¬ w = z ↔ ¬ w = y))
27		ax-8 963	. . . . . . . 8 ⊢ (x = w → (x = y → w = y))
28	27	con3d 95	. . . . . . 7 ⊢ (x = w → (¬ w = y → ¬ x = y))
29	28	a4imev 1272	. . . . . 6 ⊢ (¬ w = y → ∃x ¬ x = y)
30	26, 29	syl6bi 214	. . . . 5 ⊢ (z = y → (¬ w = z → ∃x ¬ x = y))
31		ax-8 963	. . . . . . . 8 ⊢ (x = z → (x = y → z = y))
32	31	con3d 95	. . . . . . 7 ⊢ (x = z → (¬ z = y → ¬ x = y))
33	32	a4imev 1272	. . . . . 6 ⊢ (¬ z = y → ∃x ¬ x = y)
34	33	a1d 12	. . . . 5 ⊢ (¬ z = y → (¬ w = z → ∃x ¬ x = y))
35	30, 34	pm2.61i 126	. . . 4 ⊢ (¬ w = z → ∃x ¬ x = y)
36	35	19.23aivv 1295	. . 3 ⊢ (∃w∃z ¬ w = z → ∃x ¬ x = y)
37	24, 36	ax-mp 7	. 2 ⊢ ∃x ¬ x = y
38		exnal 1037	. 2 ⊢ (∃x ¬ x = y ↔ ¬ ∀x x = y)
39	37, 38	mpbi 189	1 ⊢ ¬ ∀x x = y

Syntax hints:  ¬ wn 2   → wi 3   ⋀ wa 223  ∀wal 953   = wceq 955   ∈ wcel 957  ∃wex 979

This theorem is referenced by:  ax16b 2745

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-12 967  ax-13 968  ax-14 969  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-nul 2706  ax-pow 2738

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 980

Copyright terms: Public domain