= Solution
Use <negation introduction> on the unwanted <existential quantification>, and <existential quantifier elimination rule> with a fresh witness $a$:
``
1 ∀x. ¬P(x) premise
2 | ∃x. P(x) assumption
3 | | P(a) assumption, a fresh
4 | | ¬P(a) ∀-elim 1
5 | | ⊥ ¬-elim 3,4
6 | ⊥ ∃-elim 2,3–5
7 ¬(∃x. P(x)) ¬-intro 2–6
``
The witness name occurs neither in the surrounding assumptions nor in the conclusion $\bot$ of its <subproof>. This satisfies the <eigenvariable condition>; it is not an arbitrarily chosen fixed element assumed to witness the <existential quantification>. The result is \b[$\neg\exists x\,P(x)$].
Back to article page
