Theorem axextnd 4926

Description: A version of the Axiom of Extensionality with no distinct variable conditions.

Assertion

Ref	Expression
axextnd	⊢ ∃x((x ∈ y ↔ x ∈ z) → y = z)

Proof of Theorem axextnd

Step	Hyp	Ref	Expression
1		hbnae 1146	. . . . . . . 8 ⊢ (¬ ∀x x = y → ∀x ¬ ∀x x = y)
2		hbnae 1146	. . . . . . . 8 ⊢ (¬ ∀x x = z → ∀x ¬ ∀x x = z)
3	1, 2	hban 1008	. . . . . . 7 ⊢ ((¬ ∀x x = y ⋀ ¬ ∀x x = z) → ∀x(¬ ∀x x = y ⋀ ¬ ∀x x = z))
4		dveel2 1356	. . . . . . . . 9 ⊢ (¬ ∀x x = y → (w ∈ y → ∀x w ∈ y))
5	4	adantr 389	. . . . . . . 8 ⊢ ((¬ ∀x x = y ⋀ ¬ ∀x x = z) → (w ∈ y → ∀x w ∈ y))
6		dveel2 1356	. . . . . . . . 9 ⊢ (¬ ∀x x = z → (w ∈ z → ∀x w ∈ z))
7	6	adantl 388	. . . . . . . 8 ⊢ ((¬ ∀x x = y ⋀ ¬ ∀x x = z) → (w ∈ z → ∀x w ∈ z))
8	3, 5, 7	hbbid 1111	. . . . . . 7 ⊢ ((¬ ∀x x = y ⋀ ¬ ∀x x = z) → ((w ∈ y ↔ w ∈ z) → ∀x(w ∈ y ↔ w ∈ z)))
9		elequ1 1135	. . . . . . . . 9 ⊢ (w = x → (w ∈ y ↔ x ∈ y))
10		elequ1 1135	. . . . . . . . 9 ⊢ (w = x → (w ∈ z ↔ x ∈ z))
11	9, 10	bibi12d 628	. . . . . . . 8 ⊢ (w = x → ((w ∈ y ↔ w ∈ z) ↔ (x ∈ y ↔ x ∈ z)))
12	11	a1i 8	. . . . . . 7 ⊢ ((¬ ∀x x = y ⋀ ¬ ∀x x = z) → (w = x → ((w ∈ y ↔ w ∈ z) ↔ (x ∈ y ↔ x ∈ z))))
13	3, 8, 12	cbvald 1319	. . . . . 6 ⊢ ((¬ ∀x x = y ⋀ ¬ ∀x x = z) → (∀w(w ∈ y ↔ w ∈ z) ↔ ∀x(x ∈ y ↔ x ∈ z)))
14		zfext2 1460	. . . . . 6 ⊢ (∀w(w ∈ y ↔ w ∈ z) → y = z)
15	13, 14	syl6bir 215	. . . . 5 ⊢ ((¬ ∀x x = y ⋀ ¬ ∀x x = z) → (∀x(x ∈ y ↔ x ∈ z) → y = z))
16		19.8a 1028	. . . . 5 ⊢ (y = z → ∃x y = z)
17	15, 16	syl6 22	. . . 4 ⊢ ((¬ ∀x x = y ⋀ ¬ ∀x x = z) → (∀x(x ∈ y ↔ x ∈ z) → ∃x y = z))
18	17	ex 373	. . 3 ⊢ (¬ ∀x x = y → (¬ ∀x x = z → (∀x(x ∈ y ↔ x ∈ z) → ∃x y = z)))
19		a9e 1124	. . . . 5 ⊢ ∃x x = z
20		hbae 1144	. . . . . 6 ⊢ (∀x x = y → ∀x∀x x = y)
21		ax-8 963	. . . . . . 7 ⊢ (x = y → (x = z → y = z))
22	21	a4s 983	. . . . . 6 ⊢ (∀x x = y → (x = z → y = z))
23	20, 22	19.22d 1061	. . . . 5 ⊢ (∀x x = y → (∃x x = z → ∃x y = z))
24	19, 23	mpi 44	. . . 4 ⊢ (∀x x = y → ∃x y = z)
25	24	a1d 12	. . 3 ⊢ (∀x x = y → (∀x(x ∈ y ↔ x ∈ z) → ∃x y = z))
26		a9e 1124	. . . . 5 ⊢ ∃x x = y
27		hbae 1144	. . . . . 6 ⊢ (∀x x = z → ∀x∀x x = z)
28		ax-8 963	. . . . . . . 8 ⊢ (x = z → (x = y → z = y))
29		equcomi 1127	. . . . . . . 8 ⊢ (z = y → y = z)
30	28, 29	syl6 22	. . . . . . 7 ⊢ (x = z → (x = y → y = z))
31	30	a4s 983	. . . . . 6 ⊢ (∀x x = z → (x = y → y = z))
32	27, 31	19.22d 1061	. . . . 5 ⊢ (∀x x = z → (∃x x = y → ∃x y = z))
33	26, 32	mpi 44	. . . 4 ⊢ (∀x x = z → ∃x y = z)
34	33	a1d 12	. . 3 ⊢ (∀x x = z → (∀x(x ∈ y ↔ x ∈ z) → ∃x y = z))
35	18, 25, 34	pm2.61ii 130	. 2 ⊢ (∀x(x ∈ y ↔ x ∈ z) → ∃x y = z)
36	35	19.35ri 1076	1 ⊢ ∃x((x ∈ y ↔ x ∈ z) → y = z)

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

This theorem is referenced by:  zfcndext 4948

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-9 964  ax-10 965  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-10o 1139  ax-ext 1458

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

Copyright terms: Public domain