Metamath Proof Explorer

Theorem ac6s5

Description: Generalization of the Axiom of Choice to proper classes. B is a collection B ( x ) of nonempty, possible proper classes. Remark after Theorem 10.46 of TakeutiZaring p. 98. (Contributed by NM, 27-Mar-2006)

Ref Expression
Hypothesis ac6s4.1 ⊢ A ∈ V
Assertion ac6s5 ⊢ ∀ x ∈ A B ≠ ∅ → ∃ f ∀ x ∈ A f ⁡ x ∈ B

Proof

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