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

Metamath Proof Explorer

Theorem 2exsb

Description: An equivalent expression for double existence. (Contributed by NM, 2-Feb-2005) (Proof shortened by Wolf Lammen, 30-Sep-2018)

Ref Expression
Assertion 2exsb ⊢ ∃ x ∃ y φ ↔ ∃ z ∃ w ∀ x ∀ y x = z ∧ y = w → φ

Proof

Step Hyp Ref Expression
1 nfv ⊢ Ⅎ w φ
2 nfv ⊢ Ⅎ z φ
3 1 2 2sb8ef ⊢ ∃ x ∃ y φ ↔ ∃ z ∃ w z x w y φ
4 2sb6 ⊢ z x w y φ ↔ ∀ x ∀ y x = z ∧ y = w → φ
5 4 2exbii ⊢ ∃ z ∃ w z x w y φ ↔ ∃ z ∃ w ∀ x ∀ y x = z ∧ y = w → φ
6 3 5 bitri ⊢ ∃ x ∃ y φ ↔ ∃ z ∃ w ∀ x ∀ y x = z ∧ y = w → φ