Metamath Proof Explorer

Theorem 19.12vvv

Description: Version of 19.12vv with a disjoint variable condition, requiring fewer axioms. See also 19.12 . (Contributed by BJ, 18-Mar-2020)

Ref Expression
Assertion 19.12vvv ⊢ ∃ x ∀ y φ → ψ ↔ ∀ y ∃ x φ → ψ

Proof

Step Hyp Ref Expression
1 19.21v ⊢ ∀ y φ → ψ ↔ φ → ∀ y ψ
2 1 exbii ⊢ ∃ x ∀ y φ → ψ ↔ ∃ x φ → ∀ y ψ
3 19.36v ⊢ ∃ x φ → ∀ y ψ ↔ ∀ x φ → ∀ y ψ
4 19.36v ⊢ ∃ x φ → ψ ↔ ∀ x φ → ψ
5 4 albii ⊢ ∀ y ∃ x φ → ψ ↔ ∀ y ∀ x φ → ψ
6 19.21v ⊢ ∀ y ∀ x φ → ψ ↔ ∀ x φ → ∀ y ψ
7 5 6 bitr2i ⊢ ∀ x φ → ∀ y ψ ↔ ∀ y ∃ x φ → ψ
8 2 3 7 3bitri ⊢ ∃ x ∀ y φ → ψ ↔ ∀ y ∃ x φ → ψ