Is this deduction using =elim rule correctly written?

Question

Is this deduction correctly written as an application of =elim rule?

1. $t_1=t_3 \qquad Assumption$

2. $E\left[t_1/y_1,t_2/y_2\right]=E\left[t_1/y_1,t_2/y_2\right] \qquad = Intro$

3. $E\left[t_1/y_1,t_2/y_2\right]=E\left[t_3/y_1,t_2/y_2\right] \qquad = Elim \: 1,2$

E being an expression and $E[t_1/y_1,t_2/y_2]$ being the expression got from E by replacing each free occurrence of $y_1$ and each free occurrence of $y_2$ , in order by $t_1$ and $t_2$.

Answer 1

Ok, so $E$ is some complex term, say $E=f(y_1,y_2)$, and so on line 2 you really just have:

$f(t_1,t_2)=f(t_1,t_2)$

And on line 3, using $= Elim$ On 1 and 2, you get:

$f(t_1,t_2)=f(t_3,t_2)$

That is correct, yes.

Also, please note that you don't have to replace all occurrences of $t_1$ in $E$ with $t_3$ . If you replace just some of them, it is still a correct application of $= Elim$.