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

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 ⊢ A ∈ V
ac6s.2 ⊢ y = f ⁡ x → φ ↔ ψ
Assertion ac6s3 ⊢ ∀ x ∈ A ∃ y φ → ∃ f ∀ x ∈ A ψ

Proof

Step Hyp Ref Expression
1 ac6s.1 ⊢ A ∈ V
2 ac6s.2 ⊢ y = f ⁡ x → φ ↔ ψ
3 1 2 ac6s2 ⊢ ∀ x ∈ A ∃ y φ → ∃ f f Fn A ∧ ∀ x ∈ A ψ
4 exsimpr ⊢ ∃ f f Fn A ∧ ∀ x ∈ A ψ → ∃ f ∀ x ∈ A ψ
5 3 4 syl ⊢ ∀ x ∈ A ∃ y φ → ∃ f ∀ x ∈ A ψ