Metamath Proof Explorer

Theorem ac6c5

Description: Equivalent of Axiom of Choice. B is a collection B ( x ) of nonempty sets. Remark after Theorem 10.46 of TakeutiZaring p. 98. (Contributed by Mario Carneiro, 22-Mar-2013)

Ref Expression
Hypotheses ac6c4.1 ⊢ A ∈ V
ac6c4.2 ⊢ B ∈ V
Assertion ac6c5 ⊢ ∀ x ∈ A B ≠ ∅ → ∃ f ∀ x ∈ A f ⁡ x ∈ B

Proof

Step Hyp Ref Expression
1 ac6c4.1 ⊢ A ∈ V
2 ac6c4.2 ⊢ B ∈ V
3 1 2 ac6c4 ⊢ ∀ x ∈ A B ≠ ∅ → ∃ f f Fn A ∧ ∀ x ∈ A f ⁡ x ∈ B
4 exsimpr ⊢ ∃ f f Fn A ∧ ∀ x ∈ A f ⁡ x ∈ B → ∃ f ∀ x ∈ A f ⁡ x ∈ B
5 3 4 syl ⊢ ∀ x ∈ A B ≠ ∅ → ∃ f ∀ x ∈ A f ⁡ x ∈ B