Metamath Proof Explorer

Theorem ac6gf

Description: Axiom of Choice. (Contributed by Jeff Madsen, 2-Sep-2009)

Ref Expression
Hypotheses ac6gf.1 ⊢ Ⅎ y ψ
ac6gf.2 ⊢ y = f ⁡ x → φ ↔ ψ
Assertion ac6gf ⊢ A ∈ C ∧ ∀ x ∈ A ∃ y ∈ B φ → ∃ f f : A ⟶ B ∧ ∀ x ∈ A ψ

Proof

Step Hyp Ref Expression
1 ac6gf.1 ⊢ Ⅎ y ψ
2 ac6gf.2 ⊢ y = f ⁡ x → φ ↔ ψ
3 cbvrexsvw ⊢ ∃ y ∈ B φ ↔ ∃ z ∈ B z y φ
4 3 ralbii ⊢ ∀ x ∈ A ∃ y ∈ B φ ↔ ∀ x ∈ A ∃ z ∈ B z y φ
5 1 2 sbhypf ⊢ z = f ⁡ x → z y φ ↔ ψ
6 5 ac6sg ⊢ A ∈ C → ∀ x ∈ A ∃ z ∈ B z y φ → ∃ f f : A ⟶ B ∧ ∀ x ∈ A ψ
7 6 imp ⊢ A ∈ C ∧ ∀ x ∈ A ∃ z ∈ B z y φ → ∃ f f : A ⟶ B ∧ ∀ x ∈ A ψ
8 4 7 sylan2b ⊢ A ∈ C ∧ ∀ x ∈ A ∃ y ∈ B φ → ∃ f f : A ⟶ B ∧ ∀ x ∈ A ψ