ac2 - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
GIF version

Theorem ac2 4718

Description: Axiom of Choice equivalent. By using restricted quantifiers, we can express the Axiom of Choice with a single conjunction. (If you want to figure it out, the rewritten equivalent ac3 4719 is easier to understand.) Note: aceq0 4702 shows the logical equivalence to ax-ac 4716.

**Assertion**
Ref	Expression
ac2	⊢ ∃y∀z ∈ x ∀w ∈ z ∃!v ∈ z ∃u ∈ y (z ∈ u ⋀ v ∈ u)

Distinct variable group: x,y,z,w,v,u

**Proof of Theorem ac2**
Step	Hyp	Ref	Expression
1		ax-ac 4716	. 2 ⊢ ∃y∀z∀w((z ∈ w ⋀ w ∈ x) → ∃v∀u(∃t((u ∈ w ⋀ w ∈ t) ⋀ (u ∈ t ⋀ t ∈ y)) ↔ u = v))
2		aceq0 4702	. 2 ⊢ (∃y∀z ∈ x ∀w ∈ z ∃!v ∈ z ∃u ∈ y (z ∈ u ⋀ v ∈ u) ↔ ∃y∀z∀w((z ∈ w ⋀ w ∈ x) → ∃v∀u(∃t((u ∈ w ⋀ w ∈ t) ⋀ (u ∈ t ⋀ t ∈ y)) ↔ u = v)))
3	1, 2	mpbir 190	1 ⊢ ∃y∀z ∈ x ∀w ∈ z ∃!v ∈ z ∃u ∈ y (z ∈ u ⋀ v ∈ u)

Colors of variables: wff set class

Syntax hints: → wi 3 ↔ wb 146 ⋀ wa 223 ∀wal 951 = wceq 953 ∈ wcel 955 ∃wex 977 ∀wral 1637 ∃wrex 1638 ∃!wreu 1639

This theorem is referenced by: ac3 4719 ac7 4720

This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 959 ax-gen 960 ax-8 961 ax-10 963 ax-11 964 ax-12 965 ax-13 966 ax-14 967 ax-17 968 ax-4 970 ax-5o 972 ax-6o 975 ax-9o 1119 ax-10o 1136 ax-11o 1213 ax-ext 1452 ax-ac 4716

This theorem depends on definitions: df-bi 147 df-or 224 df-an 225 df-ex 978 df-sb 1168 df-eu 1375 df-cleq 1462 df-clel 1465 df-ral 1641 df-rex 1642 df-reu 1643