Metamath Proof Explorer


Theorem ac6s3

Description: Generalization of the Axiom of Choice to classes. Theorem 10.46 of TakeutiZaring p. 97. (Contributed by NM, 3-Nov-2004)

Ref Expression
Hypotheses ac6s.1 𝐴 ∈ V
ac6s.2 ( 𝑦 = ( 𝑓𝑥 ) → ( 𝜑𝜓 ) )
Assertion ac6s3 ( ∀ 𝑥𝐴𝑦 𝜑 → ∃ 𝑓𝑥𝐴 𝜓 )

Proof

Step Hyp Ref Expression
1 ac6s.1 𝐴 ∈ V
2 ac6s.2 ( 𝑦 = ( 𝑓𝑥 ) → ( 𝜑𝜓 ) )
3 1 2 ac6s2 ( ∀ 𝑥𝐴𝑦 𝜑 → ∃ 𝑓 ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥𝐴 𝜓 ) )
4 exsimpr ( ∃ 𝑓 ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥𝐴 𝜓 ) → ∃ 𝑓𝑥𝐴 𝜓 )
5 3 4 syl ( ∀ 𝑥𝐴𝑦 𝜑 → ∃ 𝑓𝑥𝐴 𝜓 )