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

Metamath Proof Explorer

Theorem 2nalexn

Description: Part of theorem *11.5 in WhiteheadRussell p. 164. (Contributed by Andrew Salmon, 24-May-2011)

Ref Expression
Assertion 2nalexn ⊢ ¬ ∀ x ∀ y φ ↔ ∃ x ∃ y ¬ φ

Proof

Step Hyp Ref Expression
1 df-ex ⊢ ∃ x ∃ y ¬ φ ↔ ¬ ∀ x ¬ ∃ y ¬ φ
2 alex ⊢ ∀ y φ ↔ ¬ ∃ y ¬ φ
3 2 albii ⊢ ∀ x ∀ y φ ↔ ∀ x ¬ ∃ y ¬ φ
4 1 3 xchbinxr ⊢ ∃ x ∃ y ¬ φ ↔ ¬ ∀ x ∀ y φ
5 4 bicomi ⊢ ¬ ∀ x ∀ y φ ↔ ∃ x ∃ y ¬ φ