Theorem axac 1085

Description: Axiom of Choice expressed with fewest number of different variables. The penultimate step shows the logical equivalence to ax-ac 1080.

Assertion

Ref	Expression
axac	⊢ ∃x∀y∀z((y ∈ z ∧ z ∈ w) → ∃w∀y(∃w((y ∈ z ∧ z ∈ w) ∧ (y ∈ w ∧ w ∈ x)) ↔ y = w))

Distinct variable group(s):   x,y,z,w

Proof of Theorem axac

Step	Hyp	Ref	Expression
1		ax-ac 1080	. 2 ⊢ ∃x∀y∀z((y ∈ z ∧ z ∈ w) → ∃v∀u(∃t((u ∈ z ∧ z ∈ t) ∧ (u ∈ t ∧ t ∈ x)) ↔ u = v))
2		eqt2b 818	. . . . . . . . . 10 ⊢ (v = w → (u = v ↔ u = w))
3	2	bibi2d 470	. . . . . . . . 9 ⊢ (v = w → ((∃t((u ∈ z ∧ z ∈ t) ∧ (u ∈ t ∧ t ∈ x)) ↔ u = v) ↔ (∃t((u ∈ z ∧ z ∈ t) ∧ (u ∈ t ∧ t ∈ x)) ↔ u = w)))
4		a14b 820	. . . . . . . . . . . . 13 ⊢ (t = w → (z ∈ t ↔ z ∈ w))
5	4	anbi2d 468	. . . . . . . . . . . 12 ⊢ (t = w → ((u ∈ z ∧ z ∈ t) ↔ (u ∈ z ∧ z ∈ w)))
6		a14b 820	. . . . . . . . . . . . 13 ⊢ (t = w → (u ∈ t ↔ u ∈ w))
7		a13b 819	. . . . . . . . . . . . 13 ⊢ (t = w → (t ∈ x ↔ w ∈ x))
8	6, 7	anbi12d 476	. . . . . . . . . . . 12 ⊢ (t = w → ((u ∈ t ∧ t ∈ x) ↔ (u ∈ w ∧ w ∈ x)))
9	5, 8	anbi12d 476	. . . . . . . . . . 11 ⊢ (t = w → (((u ∈ z ∧ z ∈ t) ∧ (u ∈ t ∧ t ∈ x)) ↔ ((u ∈ z ∧ z ∈ w) ∧ (u ∈ w ∧ w ∈ x))))
10	9	cbvexv 973	. . . . . . . . . 10 ⊢ (∃t((u ∈ z ∧ z ∈ t) ∧ (u ∈ t ∧ t ∈ x)) ↔ ∃w((u ∈ z ∧ z ∈ w) ∧ (u ∈ w ∧ w ∈ x)))
11	10	bibi1i 461	. . . . . . . . 9 ⊢ ((∃t((u ∈ z ∧ z ∈ t) ∧ (u ∈ t ∧ t ∈ x)) ↔ u = w) ↔ (∃w((u ∈ z ∧ z ∈ w) ∧ (u ∈ w ∧ w ∈ x)) ↔ u = w))
12	3, 11	syl6bb 414	. . . . . . . 8 ⊢ (v = w → ((∃t((u ∈ z ∧ z ∈ t) ∧ (u ∈ t ∧ t ∈ x)) ↔ u = v) ↔ (∃w((u ∈ z ∧ z ∈ w) ∧ (u ∈ w ∧ w ∈ x)) ↔ u = w)))
13	12	bialdv 935	. . . . . . 7 ⊢ (v = w → (∀u(∃t((u ∈ z ∧ z ∈ t) ∧ (u ∈ t ∧ t ∈ x)) ↔ u = v) ↔ ∀u(∃w((u ∈ z ∧ z ∈ w) ∧ (u ∈ w ∧ w ∈ x)) ↔ u = w)))
14		a13b 819	. . . . . . . . . . . 12 ⊢ (u = y → (u ∈ z ↔ y ∈ z))
15	14	anbi1d 469	. . . . . . . . . . 11 ⊢ (u = y → ((u ∈ z ∧ z ∈ w) ↔ (y ∈ z ∧ z ∈ w)))
16		a13b 819	. . . . . . . . . . . 12 ⊢ (u = y → (u ∈ w ↔ y ∈ w))
17	16	anbi1d 469	. . . . . . . . . . 11 ⊢ (u = y → ((u ∈ w ∧ w ∈ x) ↔ (y ∈ w ∧ w ∈ x)))
18	15, 17	anbi12d 476	. . . . . . . . . 10 ⊢ (u = y → (((u ∈ z ∧ z ∈ w) ∧ (u ∈ w ∧ w ∈ x)) ↔ ((y ∈ z ∧ z ∈ w) ∧ (y ∈ w ∧ w ∈ x))))
19	18	biexdv 936	. . . . . . . . 9 ⊢ (u = y → (∃w((u ∈ z ∧ z ∈ w) ∧ (u ∈ w ∧ w ∈ x)) ↔ ∃w((y ∈ z ∧ z ∈ w) ∧ (y ∈ w ∧ w ∈ x))))
20		a8b 817	. . . . . . . . 9 ⊢ (u = y → (u = w ↔ y = w))
21	19, 20	bibi12d 477	. . . . . . . 8 ⊢ (u = y → ((∃w((u ∈ z ∧ z ∈ w) ∧ (u ∈ w ∧ w ∈ x)) ↔ u = w) ↔ (∃w((y ∈ z ∧ z ∈ w) ∧ (y ∈ w ∧ w ∈ x)) ↔ y = w)))
22	21	cbvalv 972	. . . . . . 7 ⊢ (∀u(∃w((u ∈ z ∧ z ∈ w) ∧ (u ∈ w ∧ w ∈ x)) ↔ u = w) ↔ ∀y(∃w((y ∈ z ∧ z ∈ w) ∧ (y ∈ w ∧ w ∈ x)) ↔ y = w))
23	13, 22	syl6bb 414	. . . . . 6 ⊢ (v = w → (∀u(∃t((u ∈ z ∧ z ∈ t) ∧ (u ∈ t ∧ t ∈ x)) ↔ u = v) ↔ ∀y(∃w((y ∈ z ∧ z ∈ w) ∧ (y ∈ w ∧ w ∈ x)) ↔ y = w)))
24	23	cbvexv 973	. . . . 5 ⊢ (∃v∀u(∃t((u ∈ z ∧ z ∈ t) ∧ (u ∈ t ∧ t ∈ x)) ↔ u = v) ↔ ∃w∀y(∃w((y ∈ z ∧ z ∈ w) ∧ (y ∈ w ∧ w ∈ x)) ↔ y = w))
25	24	imbi2i 160	. . . 4 ⊢ (((y ∈ z ∧ z ∈ w) → ∃v∀u(∃t((u ∈ z ∧ z ∈ t) ∧ (u ∈ t ∧ t ∈ x)) ↔ u = v)) ↔ ((y ∈ z ∧ z ∈ w) → ∃w∀y(∃w((y ∈ z ∧ z ∈ w) ∧ (y ∈ w ∧ w ∈ x)) ↔ y = w)))
26	25	bi2al 696	. . 3 ⊢ (∀y∀z((y ∈ z ∧ z ∈ w) → ∃v∀u(∃t((u ∈ z ∧ z ∈ t) ∧ (u ∈ t ∧ t ∈ x)) ↔ u = v)) ↔ ∀y∀z((y ∈ z ∧ z ∈ w) → ∃w∀y(∃w((y ∈ z ∧ z ∈ w) ∧ (y ∈ w ∧ w ∈ x)) ↔ y = w)))
27	26	biex 733	. 2 ⊢ (∃x∀y∀z((y ∈ z ∧ z ∈ w) → ∃v∀u(∃t((u ∈ z ∧ z ∈ t) ∧ (u ∈ t ∧ t ∈ x)) ↔ u = v)) ↔ ∃x∀y∀z((y ∈ z ∧ z ∈ w) → ∃w∀y(∃w((y ∈ z ∧ z ∈ w) ∧ (y ∈ w ∧ w ∈ x)) ↔ y = w)))
28	1, 27	mpbi 164	1 ⊢ ∃x∀y∀z((y ∈ z ∧ z ∈ w) → ∃w∀y(∃w((y ∈ z ∧ z ∈ w) ∧ (y ∈ w ∧ w ∈ x)) ↔ y = w))

Syntax hints:   → wi 2   ↔ wb 127   ∧ wa 196  ∀wal 672  ∃wex 678   = weq 797   ∈ wel 803

This theorem is referenced by:  axacndlem4 3756

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-12 802  ax-13 804  ax-14 805  ax-17 925  ax-ac 1080

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679

metamath.org