Metamath Proof Explorer

Theorem ac6sg

Description: ac6s with sethood as antecedent. (Contributed by FL, 3-Aug-2009)

Ref Expression
Hypothesis ac6sg.1 ⊢ y = f ⁡ x → φ ↔ ψ
Assertion ac6sg ⊢ A ∈ V → ∀ x ∈ A ∃ y ∈ B φ → ∃ f f : A ⟶ B ∧ ∀ x ∈ A ψ

Proof

Step Hyp Ref Expression
1 ac6sg.1 ⊢ y = f ⁡ x → φ ↔ ψ
2 raleq ⊢ z = A → ∀ x ∈ z ∃ y ∈ B φ ↔ ∀ x ∈ A ∃ y ∈ B φ
3 feq2 ⊢ z = A → f : z ⟶ B ↔ f : A ⟶ B
4 raleq ⊢ z = A → ∀ x ∈ z ψ ↔ ∀ x ∈ A ψ
5 3 4 anbi12d ⊢ z = A → f : z ⟶ B ∧ ∀ x ∈ z ψ ↔ f : A ⟶ B ∧ ∀ x ∈ A ψ
6 5 exbidv ⊢ z = A → ∃ f f : z ⟶ B ∧ ∀ x ∈ z ψ ↔ ∃ f f : A ⟶ B ∧ ∀ x ∈ A ψ
7 2 6 imbi12d ⊢ z = A → ∀ x ∈ z ∃ y ∈ B φ → ∃ f f : z ⟶ B ∧ ∀ x ∈ z ψ ↔ ∀ x ∈ A ∃ y ∈ B φ → ∃ f f : A ⟶ B ∧ ∀ x ∈ A ψ
8 vex ⊢ z ∈ V
9 8 1 ac6s ⊢ ∀ x ∈ z ∃ y ∈ B φ → ∃ f f : z ⟶ B ∧ ∀ x ∈ z ψ
10 7 9 vtoclg ⊢ A ∈ V → ∀ x ∈ A ∃ y ∈ B φ → ∃ f f : A ⟶ B ∧ ∀ x ∈ A ψ