Universal elimination when $\forall$ is not the main operator

Question

I was asked to apply universal elimination on $\forall x A(x) \rightarrow B,$ but the $\forall$ here is not the main operator, what should I do? here's the question and what I have for now

Answer 1

Universal elimination when $∀$ is not the main operator.

You cannot apply UE when the quantifier is not the main operator.

You have to derive $\forall x A(x)$ in order to use it to "detach" $B$ using ($\to$-E):

1. $\forall x A(x) \to B$ --- premise

2. $\lnot \exists x (A(x) \to B)$ --- assumed [a]

3. $\lnot A(y)$ --- assumed [b]

4. $A(y)$ --- assumed [c]

5. $\bot$

6. $B$ --- from 5)

7. $A(y) \to B$ --- from 4) and 6) by ($\to$-I), discharging [c]

8. $\exists x (A(x) \to B)$ --- from 7) by ($\exists$-I)

9. $\bot$

10. $\lnot \lnot A(y)$ --- from 3) and 9) by ($\to$-I), discharging [b]

11. $A(y)$ --- from 10) by ($\lnot \lnot$-E)

12. $\forall x A(x)$ --- from 11) by ($\forall$-I)

13. $B$ --- from 1) and 12) by ($\to$-E)

14. $A(y) \to B$ --- from 13) by ($\to$-I)

15. $\exists x (A(x) \to B)$ --- from 14) by ($\exists$-I)

16. $\bot$

17. $\exists x (A(x) \to B)$ --- from 2) and 16) by ($\to$-I), discharging [a], followed by ($\lnot \lnot$-E)