As long as you restrict yourself to sentences (so all of propositional logic, but also formulas in quantificational logic without any free variables), then these substitutions are indeed perfectly logically valid, and several texts prove a kind of 'Substitution Theorem' or 'Replacement Theorem' to this effect.
Moreover, there are formal proof systems that allow you to do this kind of thing. Some proof systems have a set of predefined logical equivalences (such as Double Negation, DeMorgan, Commutation, Association, Distribution, etc.) that can be used as inferences in a proof (see for example Copi's formal proof systems) and I know I have seen proof systems where any earlier proven equivalence can be used as a 'substitution' inference in other proofs.
When it comes to formulas in general (where you can have free variables) you need to be a little more careful, as you already realized (although I cannot quite follow your example ...). However, we can still a few things as far as equivalences and substitutions go.
First of all, as long as no variables are changed, we can easily extend the propositional logic equivalences to formulas. Thus, we can say that $Happy(x) \Leftrightarrow \neg \neg Happy(x)$, and since we can likewise extend the 'Substitution Theorem' to formulas, we can therefore infer $\forall x \ \neg \neg Happy(x)$ from $\forall x \ Happy(x)$.
When variables are changed, though, things get more tricky. In fact, it may seem that $Happy(x)$ is logically equivalent to $Happy(y)$, but clearly you cannot infer $\forall x \ Happy(y)$ from $\forall x \ Happy(x)$. Fortunately, it turns out that $Happy(x)$ not logically equivalent to $Happy(y)$ anyway, as we define the logical equivalence of formulas in terms of variable assignments (functions that map variables to objects in the domain) and as such I can map $x$ to a different object than $y$, and thereby demonstrate their non-equivalence.
Nevertheless, there still are equivalences that involve changing variables: $\forall x \ Happy(x)$ is equivalent to $\forall y \ Happy(y)$. Indeed, there is a general 'Replacing Bound variables' equivalence principle:
Replacing Bound variables
Where $\varphi(x)$ and $\varphi(y)$ are any FOL formulas, and where $\varphi(x)$ would be the result of replacing all free variables of $y$ in $\varphi(y)$, and where $\varphi(y)$ would be the result of replacing all free variables of $x$ in $\varphi(x)$:
$\forall x \ \varphi(x) \Leftrightarrow \forall y \ \varphi(y)$
$\exists x \ \varphi(x) \Leftrightarrow \exists y \ \varphi(y)$
In sum, then, as long as you have a good definition of logical equivalence of formulas, then there is indeed a general Substitution Principle of exactly the kind you suggest, and you could even make that into a formal inference rule.
A priori, you are right, there might be a problem in the rules $\land_E$ and $\to_E$, because the . But in fact, the problem is easily solved because there is another nice property for natural deduction:
Lemma: If $\Gamma \vdash \varphi$ and $x \in FV(\varphi)$ then $x \in FV(\psi)$ for some $\psi \in \Gamma$.
This lemma can be easily proved by induction on the derivation of $\Gamma \vdash \varphi$ (if you prefer, you can prove it simultaneously to the proof of van Dalen's Theorem 2.8.3.(i)). Note that you are in language where the only connectives are $\land, \to, ⊥$ and $\forall$ (p. 91).
Thanks to the lemma above, you do not have any problem in the proof of Theorem 2.8.3.(i) with the cases $\land_E$ and $\to_E$. For instance, for $\land_{E_i}$ (with $i \in \{1,2\}$), you have that
\begin{align}
\dfrac{\quad\Gamma\\\quad \ \vdots\\\varphi_1 \land \varphi_2}{\varphi_i}\land_{E_i}
\end{align}
According to your hypothesis, $x$ does not occur in $\Gamma$ or $\varphi_i$, but what about $\varphi_j$ with $j\neq i$?
By the lemma above, if $x$ occurred free in $\varphi_j$ then $x$ would occur free in $\Gamma$, which contradicts the hypothesis. So, $x \notin FV(\varphi_j)$.
Moreover, if $x$ occurred bound in $\varphi_j$ then you could rename bound variables in $\varphi_j$ so that $x$ does not occur bound in $\varphi_j$.
Therefore, $x$ do not occur in $\Gamma$ or $\varphi_1$ or $\varphi_2$. Hence, you can apply the inductive hypothesis to the derivation of $\Gamma \vdash \varphi \land \varphi_2$. Then, you can easily conclude by yourself.
Best Answer
Using the given Identity Axioms:
(E1) $\forall x \exists y (x=y)$
If (E1) is not true, then Axiom I1:
$\forall x (x = x)$
will not be true. By Contradiction, (E1) is true.
(E2) It looks like we can not show this with Only the Identity Axioms; There may be more Axioms listed earlier in the Text Book, which, together with Axioms I1 & I4, must be used in (E2) here.
I think that (E2) is trying to state that variable $x$ can be substituted by variable $y$ in a statement, Provided that $y$ does not occur in the statement.
Eg $x=zx+1$ is equivalent to $y=zy+1$, but $x=yx+1$ is not equivalent to $y=yy+1$
UPDATE:
The first Part of (E2) can be shown via "Contradiction", with DeMorgans Laws:
$\varphi(x) \Leftrightarrow \exists x (x=y \land \varphi(y))$
When LHS is true, RHS must be true. Assume RHS is not true; then the negation is true.
$\lnot (\exists x (x=y \land \varphi(y)))$
$\forall x ( \lnot (x=y) \lor \lnot(\varphi(y)))$
$( \forall x \lnot (x=y) \lor \forall x \lnot(\varphi(y)))$
By (E1), $\forall x \lnot (x=y)$ is not true.
Thus, $\forall x \lnot(\varphi(y))$ must be true.
By given LHS, there is $\varphi(x)$, then $\forall x \lnot(\varphi(y))$ is not true.
It is a "Contradiction" here.
Thus Negation of RHS is not true.
Hence, RHS is true.
Here $\varphi(x)$ must not have $y$, because that might make this argument invalid:
$\varphi(x) : x=z+1$ can have at least one Integer Solution, and $\varphi(x)$ does not have $y$.
$\varphi(y) : y=z+1$ is same.
But:
$\varphi(x) : x=y+1$ can have at least one Integer Solution, but $\varphi(x)$ does have $y$.
$\varphi(y) : y=y+1$ is not the same and has no Integer Solutions.
Alternate Proof of (E2) with I4:
We could take I4 with $n=1$ to get:
$\forall x,y (x=y \rightarrow (\varphi(x) \rightarrow \varphi(y))) $
$\forall x,y ((x=y \land \varphi(x)) \rightarrow (\varphi(y))) $
$\forall x,y ((\varphi(x) \land x=y) \rightarrow (\varphi(y))) $
$\forall x (\varphi(x) \rightarrow \exists y (x=y \land \varphi(y))) $