Here are the definitions of the rules:
This answer helped me to prove the $\exists$-$I$ rule, but im struggling to prove $\exists$-$E$ How to show that the introduction and elimination rules for $\exists$ can be derived from the rules for $\forall$?
So basically, im supposed to show that given $\neg\forall x\neg A(x)$ and a subproof having $A(a)$ as a premise and proving $C$, that we may conclude $C$?
So i should probably start my assuming $\neg\forall x\neg A(x)$ and that there's a subproof that proves $A(a)\rightarrow C$? But I cant figure out what to do next.
Btw, is $A(a)\rightarrow C$ valid? Wouldnt that mean $\exists x(A(x)\rightarrow C)$, which then also means $\neg\forall x\neg (A(x)\rightarrow C)$ Maybe I could do something with that?
