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
$$\vDash \exists xA[x/z]\leftrightarrow \exists yA[y/z]\mathit{\hspace{1em}\hspace{1em}}\text{and}\mathit{\hspace{1em}\hspace{1em}}\vDash \forall xA[x/z]\leftrightarrow \forall yA[y/z]$$ 
2.

–
$\vDash ({t}_{1}={t}_{2})\to (s[{t}_{1}/x]=s[{t}_{2}/x])$

–
$\vDash ({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 $\vDash A\leftrightarrow {A}^{\prime}$ such that ${A}^{\prime}$ contains no variables that are both free and bound.
Title  semantic properties of substitutability 

Canonical name  SemanticPropertiesOfSubstitutability 
Date of creation  20130322 19:36:00 
Last modified on  20130322 19:36:00 
Owner  CWoo (3771) 
Last modified by  CWoo (3771) 
Numerical id  6 
Author  CWoo (3771) 
Entry type  Result 
Classification  msc 03B10 
Classification  msc 03B05 
\@unrecurse 