Metamath Proof Explorer

Theorem 19.12b

Description: Version of 19.12vv with not-free hypotheses, instead of distinct variable conditions. (Contributed by Scott Fenton, 13-Dec-2010) (Revised by Mario Carneiro, 11-Dec-2016)

Ref Expression
Hypotheses 19.12b.1 ⊢ Ⅎ y φ
19.12b.2 ⊢ Ⅎ x ψ
Assertion 19.12b ⊢ ∃ x ∀ y φ → ψ ↔ ∀ y ∃ x φ → ψ

Proof

Step Hyp Ref Expression
1 19.12b.1 ⊢ Ⅎ y φ
2 19.12b.2 ⊢ Ⅎ x ψ
3 1 19.21 ⊢ ∀ y φ → ψ ↔ φ → ∀ y ψ
4 3 exbii ⊢ ∃ x ∀ y φ → ψ ↔ ∃ x φ → ∀ y ψ
5 2 nfal ⊢ Ⅎ x ∀ y ψ
6 5 19.36 ⊢ ∃ x φ → ∀ y ψ ↔ ∀ x φ → ∀ y ψ
7 2 19.36 ⊢ ∃ x φ → ψ ↔ ∀ x φ → ψ
8 7 albii ⊢ ∀ y ∃ x φ → ψ ↔ ∀ y ∀ x φ → ψ
9 1 nfal ⊢ Ⅎ y ∀ x φ
10 9 19.21 ⊢ ∀ y ∀ x φ → ψ ↔ ∀ x φ → ∀ y ψ
11 8 10 bitr2i ⊢ ∀ x φ → ∀ y ψ ↔ ∀ y ∃ x φ → ψ
12 4 6 11 3bitri ⊢ ∃ x ∀ y φ → ψ ↔ ∀ y ∃ x φ → ψ