semantic properties of substitutability

In addition, we also have the following semantic properties on substitutability:

1.
If $x, y$ are respectively free for $z$ in $A$ , and do not occur free in $A$ , then
$\\models\\exists xA[x/z]\\leftrightarrow\\exists yA[y/z]\\qquad\\mbox{and}\\qquad%\\models\\forall xA[x/z]\\leftrightarrow\\forall yA[y/z]$
2.
(substitution theorem)
- –
  $\\models(t_{1}=t_{2})\\to(s[t_{1}/x]=s[t_{2}/x])$
- –
  $\\models(t_{1}=t_{2})\\to(A[t_{1}/x]=A[t_{2}/x])$
3.
Every wff $A$ is equivalent to a wff $A^{\\prime}$ in the sense $\\models A\\leftrightarrow A^{\\prime}$ such that $A^{\\prime}$ contains no variables that are both free and bound.