Theorem ac8prim

Description: ac8 expanded into primitives. (Contributed by Eric Schmidt, 19-Oct-2025)

	Ref	Expression
Assertion	ac8prim	⊢ ( ( ∀ 𝑧 ( 𝑧 ∈ 𝑥 → ∃ 𝑤 𝑤 ∈ 𝑧 ) ∧ ∀ 𝑧 ∀ 𝑤 ( ( 𝑧 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥 ) → ( ¬ 𝑧 = 𝑤 → ∀ 𝑦 ( 𝑦 ∈ 𝑧 → ¬ 𝑦 ∈ 𝑤 ) ) ) ) → ∃ 𝑦 ∀ 𝑧 ( 𝑧 ∈ 𝑥 → ∃ 𝑤 ∀ 𝑣 ( ( 𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦 ) ↔ 𝑣 = 𝑤 ) ) )

Proof

Step	Hyp	Ref	Expression
1		dfac5prim	⊢ ( CHOICE ↔ ∀ 𝑥 ( ( ∀ 𝑧 ( 𝑧 ∈ 𝑥 → ∃ 𝑤 𝑤 ∈ 𝑧 ) ∧ ∀ 𝑧 ∀ 𝑤 ( ( 𝑧 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥 ) → ( ¬ 𝑧 = 𝑤 → ∀ 𝑦 ( 𝑦 ∈ 𝑧 → ¬ 𝑦 ∈ 𝑤 ) ) ) ) → ∃ 𝑦 ∀ 𝑧 ( 𝑧 ∈ 𝑥 → ∃ 𝑤 ∀ 𝑣 ( ( 𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦 ) ↔ 𝑣 = 𝑤 ) ) ) )
2	1	axaci	⊢ ( ( ∀ 𝑧 ( 𝑧 ∈ 𝑥 → ∃ 𝑤 𝑤 ∈ 𝑧 ) ∧ ∀ 𝑧 ∀ 𝑤 ( ( 𝑧 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥 ) → ( ¬ 𝑧 = 𝑤 → ∀ 𝑦 ( 𝑦 ∈ 𝑧 → ¬ 𝑦 ∈ 𝑤 ) ) ) ) → ∃ 𝑦 ∀ 𝑧 ( 𝑧 ∈ 𝑥 → ∃ 𝑤 ∀ 𝑣 ( ( 𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦 ) ↔ 𝑣 = 𝑤 ) ) )