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 𝐴 ∈ V
ac6c4.2 𝐵 ∈ V
Assertion ac6c5 ( ∀ 𝑥𝐴 𝐵 ≠ ∅ → ∃ 𝑓𝑥𝐴 ( 𝑓𝑥 ) ∈ 𝐵 )

Proof

Step Hyp Ref Expression
1 ac6c4.1 𝐴 ∈ V
2 ac6c4.2 𝐵 ∈ V
3 1 2 ac6c4 ( ∀ 𝑥𝐴 𝐵 ≠ ∅ → ∃ 𝑓 ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥𝐴 ( 𝑓𝑥 ) ∈ 𝐵 ) )
4 exsimpr ( ∃ 𝑓 ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥𝐴 ( 𝑓𝑥 ) ∈ 𝐵 ) → ∃ 𝑓𝑥𝐴 ( 𝑓𝑥 ) ∈ 𝐵 )
5 3 4 syl ( ∀ 𝑥𝐴 𝐵 ≠ ∅ → ∃ 𝑓𝑥𝐴 ( 𝑓𝑥 ) ∈ 𝐵 )