uq_neg

Theorem uq_neg

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

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