I require clarification on the Existential rule E4 in Eliot Mendelson's Introduction to Mathematical Logic, page 61:
Let $t$ be a term that is free for $x$ in a wf $A(x,t)$, and let $A(t,t)$ arise from $A(x,t)$ by replacing all free occurrences of $x$ by $t$. Then $(\exists x)A(x,t)$ is provable from $A(t,t)$.
I think it might be more commonly known as existential introduction?
When you use the existential rule, for example, if you have a $2$-place predicate $A(x,x)$, do you have to change the variables to terms? Or can they stay variables? And more specifically, if you have a $2$-place predicate $A(x,x)$ can you do this: $(\exists y)A(x,y)$?