On the application of $\forall\mathbf{I}$ rule

Question

Trying to prove this statement.

In this example, $\forall\mathbf{I}$ would have two restrictions:

• a must not occur in any undischarged assumption
• y must not occur in A(...c...c...)

As I see it, this application is not against those rules. What's the problem, here ?

Answer 1

In this example, $∀\,\sf I$ would have two restrictions:

• $a$ must not occur in any undischarged assumption

But, $a$ does occur within $Dba$, on line 3, and that was an undischarged assumption when you tried to use universal introduction on line 4.

Thus that attempt is invalid.