neg_uq

Theorem neg_uq

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

Proof
01. 1 ⊢ ¬∀x. P x, hypo.
02. 2 ⊢ ¬∃x. ¬P x, hypo.
03. 2 ⊢ ∀x. ¬¬P x, neg_ex 2.
04. 2 ⊢ ¬¬P x, uq_elim 3.
05. 2 ⊢ P x, dne 4.
06. 2 ⊢ ∀x. P x, uq_intro 5.
07. 1, 2 ⊢ ⊥, neg_elim 1 6.
08. 1 ⊢ ¬¬∃x. ¬P x, neg_intro 7.
09. 1 ⊢ ∃x. ¬P x, dne 8.
neg_uq. ⊢ (¬∀x. P x) → (∃x. ¬P x), subj_intro 9.

Dependencies
The given proof depends on two axioms:
efq, lem.