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 𝐴 ∈ V
Assertion ac6s4 ( ∀ 𝑥𝐴 𝐵 ≠ ∅ → ∃ 𝑓 ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥𝐴 ( 𝑓𝑥 ) ∈ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 ac6s4.1 𝐴 ∈ V
2 n0 ( 𝐵 ≠ ∅ ↔ ∃ 𝑦 𝑦𝐵 )
3 2 ralbii ( ∀ 𝑥𝐴 𝐵 ≠ ∅ ↔ ∀ 𝑥𝐴𝑦 𝑦𝐵 )
4 eleq1 ( 𝑦 = ( 𝑓𝑥 ) → ( 𝑦𝐵 ↔ ( 𝑓𝑥 ) ∈ 𝐵 ) )
5 1 4 ac6s2 ( ∀ 𝑥𝐴𝑦 𝑦𝐵 → ∃ 𝑓 ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥𝐴 ( 𝑓𝑥 ) ∈ 𝐵 ) )
6 3 5 sylbi ( ∀ 𝑥𝐴 𝐵 ≠ ∅ → ∃ 𝑓 ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥𝐴 ( 𝑓𝑥 ) ∈ 𝐵 ) )