This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ac8

Description: An Axiom of Choice equivalent. Given a family x of mutually disjoint nonempty sets, there exists a set y containing exactly one member from each set in the family. Theorem 6M(4) of Enderton p. 151. (Contributed by NM, 14-May-2004)

		Ref	Expression
	Assertion	ac8	⊢ ( ( ∀ 𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) )

Proof

Step	Hyp	Ref	Expression
1		dfac5	⊢ ( CHOICE ↔ ∀ 𝑥 ( ( ∀ 𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) )
2	1	axaci	⊢ ( ( ∀ 𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) )