ex_neg

Theorem ex_neg

Theorem. ex_neg
(∃x. ¬P x) → (¬∀x. P x)

Proof
01. 1 ⊢ ∃x. ¬P x, hypo.
02. 2 ⊢ ¬P u, hypo.
03. 3 ⊢ ∀x. P x, hypo.
04. 3 ⊢ P u, uq_elim 3.
05. 3, 2 ⊢ ⊥, neg_elim 2 4.
06. 1, 3 ⊢ ⊥, ex_elim 1 5.
07. 1 ⊢ ¬∀x. P x, neg_intro 6.
ex_neg. ⊢ (∃x. ¬P x) → (¬∀x. P x), subj_intro 7.