Theorem neg_ex_bounded

Proof
01. 1 ⊢ ¬∃x. P x ∧ Q x, hypo.
02. 1 ⊢ ∀x. ¬(P x ∧ Q x), neg_ex 1.
03. 1 ⊢ ¬(P x ∧ Q x), uq_elim 2.
04. 1 ⊢ ¬P x ∨ ¬Q x, neg_conj 3.
05. 1 ⊢ P x → ¬Q x, subj_from_disj 4.
06. 1 ⊢ ∀x. P x → ¬Q x, uq_intro 5.
neg_ex_bounded. ⊢ (¬∃x. P x ∧ Q x) → (∀x. P x → ¬Q x), subj_intro 6.

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