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	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ≠ ∅ → ∃ 𝑓 ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 )