Metamath Proof Explorer

Theorem 2exbi

Description: Theorem *11.341 in WhiteheadRussell p. 162. Theorem 19.18 of Margaris p. 90 with 2 quantifiers. (Contributed by Andrew Salmon, 24-May-2011)

Ref Expression
Assertion 2exbi ⊢ ∀ x ∀ y φ ↔ ψ → ∃ x ∃ y φ ↔ ∃ x ∃ y ψ

Proof

Step Hyp Ref Expression
1 exbi ⊢ ∀ y φ ↔ ψ → ∃ y φ ↔ ∃ y ψ
2 1 alimi ⊢ ∀ x ∀ y φ ↔ ψ → ∀ x ∃ y φ ↔ ∃ y ψ
3 exbi ⊢ ∀ x ∃ y φ ↔ ∃ y ψ → ∃ x ∃ y φ ↔ ∃ x ∃ y ψ
4 2 3 syl ⊢ ∀ x ∀ y φ ↔ ψ → ∃ x ∃ y φ ↔ ∃ x ∃ y ψ