This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ac6s4

Description: Generalization of the Axiom of Choice to proper classes. B is a collection B ( x ) of nonempty, possible proper classes. (Contributed by NM, 29-Sep-2006)

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

Proof

Step Hyp Ref Expression
1 ac6s4.1 ⊢ A ∈ V
2 n0 ⊢ B ≠ ∅ ↔ ∃ y y ∈ B
3 2 ralbii ⊢ ∀ x ∈ A B ≠ ∅ ↔ ∀ x ∈ A ∃ y y ∈ B
4 eleq1 ⊢ y = f ⁡ x → y ∈ B ↔ f ⁡ x ∈ B
5 1 4 ac6s2 ⊢ ∀ x ∈ A ∃ y y ∈ B → ∃ f f Fn A ∧ ∀ x ∈ A f ⁡ x ∈ B
6 3 5 sylbi ⊢ ∀ x ∈ A B ≠ ∅ → ∃ f f Fn A ∧ ∀ x ∈ A f ⁡ x ∈ B