Metamath Proof Explorer

Theorem ac5

Description: An Axiom of Choice equivalent: there exists a function f (called a choice function) with domain A that maps each nonempty member of the domain to an element of that member. Axiom AC of BellMachover p. 488. Note that the assertion that f be a function is not necessary; see ac4 . (Contributed by NM, 29-Aug-1999)

Ref Expression
Hypothesis ac5.1 ⊢ A ∈ V
Assertion ac5 ⊢ ∃ f f Fn A ∧ ∀ x ∈ A x ≠ ∅ → f ⁡ x ∈ x

Proof

Step Hyp Ref Expression
1 ac5.1 ⊢ A ∈ V
2 fneq2 ⊢ y = A → f Fn y ↔ f Fn A
3 raleq ⊢ y = A → ∀ x ∈ y x ≠ ∅ → f ⁡ x ∈ x ↔ ∀ x ∈ A x ≠ ∅ → f ⁡ x ∈ x
4 2 3 anbi12d ⊢ y = A → f Fn y ∧ ∀ x ∈ y x ≠ ∅ → f ⁡ x ∈ x ↔ f Fn A ∧ ∀ x ∈ A x ≠ ∅ → f ⁡ x ∈ x
5 4 exbidv ⊢ y = A → ∃ f f Fn y ∧ ∀ x ∈ y x ≠ ∅ → f ⁡ x ∈ x ↔ ∃ f f Fn A ∧ ∀ x ∈ A x ≠ ∅ → f ⁡ x ∈ x
6 dfac4 ⊢ CHOICE ↔ ∀ y ∃ f f Fn y ∧ ∀ x ∈ y x ≠ ∅ → f ⁡ x ∈ x
7 6 axaci ⊢ ∃ f f Fn y ∧ ∀ x ∈ y x ≠ ∅ → f ⁡ x ∈ x
8 1 5 7 vtocl ⊢ ∃ f f Fn A ∧ ∀ x ∈ A x ≠ ∅ → f ⁡ x ∈ x