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

Metamath Proof Explorer

Theorem ac6sf2

Description: Alternate version of ac6 with bound-variable hypothesis. (Contributed by NM, 2-Mar-2008) (Revised by Thierry Arnoux, 17-May-2020)

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

Proof

Step Hyp Ref Expression
1 ac6sf2.y ⊢ Ⅎ _ y B
2 ac6sf2.1 ⊢ Ⅎ y ψ
3 ac6sf2.2 ⊢ A ∈ V
4 ac6sf2.3 ⊢ y = f ⁡ x → φ ↔ ψ
5 nfcv ⊢ Ⅎ _ z B
6 nfv ⊢ Ⅎ z φ
7 nfs1v ⊢ Ⅎ y z y φ
8 sbequ12 ⊢ y = z → φ ↔ z y φ
9 1 5 6 7 8 cbvrexfw ⊢ ∃ y ∈ B φ ↔ ∃ z ∈ B z y φ
10 9 ralbii ⊢ ∀ x ∈ A ∃ y ∈ B φ ↔ ∀ x ∈ A ∃ z ∈ B z y φ
11 2 4 sbhypf ⊢ z = f ⁡ x → z y φ ↔ ψ
12 3 11 ac6s ⊢ ∀ x ∈ A ∃ z ∈ B z y φ → ∃ f f : A ⟶ B ∧ ∀ x ∈ A ψ
13 10 12 sylbi ⊢ ∀ x ∈ A ∃ y ∈ B φ → ∃ f f : A ⟶ B ∧ ∀ x ∈ A ψ