neg_ex

Theorem neg_ex

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

Proof
01. 1 ⊢ ¬∃x. P x, hypo.
02. 2 ⊢ P x, hypo.
03. 2 ⊢ ∃x. P x, ex_intro 2.
04. 1, 2 ⊢ ⊥, neg_elim 1 3.
05. 1 ⊢ ¬P x, neg_intro 4.
06. 1 ⊢ ∀x. ¬P x, uq_intro 5.
neg_ex. ⊢ (¬∃x. P x) → (∀x. ¬P x), subj_intro 6.