= Solution
Use a fresh witness $a$ in the <existential elimination> subproof. The <universal elimination> step gives the opposite of its assumed negated property.
``
1. ∀x R(x) premise
2. ∃y ¬R(y) assumption [i]
3. ¬R(a) fresh witness assumption [j]
4. R(a) ∀E, 1
5. ⊥ ¬E, 3, 4
6. ⊥ ∃E, 2, 3–5, discharging [j]
7. ¬∃y ¬R(y) ¬I, 2–6, discharging [i]
``
The witness $a$ is absent from the premise and from the conclusion of the existential-elimination step, so its freshness condition is met.
Back to article page
