I've been looking over the Metamath Proof Explorer definitions list, and I've been having trouble understanding the definition for proper substitution. According to Metamath, the definition of proper substitution (df-sb) is given as $$\text{(df-sb) }[y/x]\phi\leftrightarrow((x=y\rightarrow\phi)\wedge\exists x(x=y\wedge\phi))\text{,}$$ where $[y/x]\phi$ is read as "the wff that results from the proper substitution of $$ for $$ in the wff $\phi$", and where $x$ and $y$ are variables ranging over sets and $\phi$ is the some wff that might contain the variables $x$ or $y$ (or both).
What I'm confused about is the use of the conjunction. It seems like only the first conjunct, $(x=y\rightarrow\phi)$, is necessary to define proper substitution. As stated by the definition description, the conjunction allows $x$ and $y$ to be substituted with the same variable by making $x$ free in the first conjunct and bounded in the second conjunct, $\exists x(x=y\wedge\phi)$, that is, $$[x/x]\phi\leftrightarrow((x=x\rightarrow\phi)\wedge\exists x(x=x\wedge\phi))$$ would hold, but why is this?
An alternate definition (sb6), similar to what I'm talking about, is also given: $$\text{(sb6) }[y/x]\phi\leftrightarrow\forall x(x=y\rightarrow\phi)\text{,}$$ where the syntax and variables are interpreted and defined like df-sb above except $x$ and $y$ are required to be distinct, that is, $$[x/x]\phi\leftrightarrow\forall x(x=x\rightarrow\phi)$$ would not hold. But why so? What is the importance of making sure $x$ and $y$ aren't the same variable?
My primary questions are:
Why is the right conjunct necessary in df-sb?
If we don't add the right conjunct in df-sb, why would the definition fail? Can you give an easy example of a proposition $\phi$ which would fail without the right conjunct?
How does having $x$ free in the left conjunct and bounded in the right conjunct allow $x$ and $y$ to be substituted for the same variable as per definition description?
Why is it necessary that $x$ and $y$ be distinct in sb6?
If we allow $x$ and $y$ to be the same variable in sb6, why would the definition fail? Can you give an easy example of a proposition $\phi$ which would fail when $x$ and $y$ are the same variable.
Is $x$ being bounded by the universal quantifier in sb6 necessary?
The key point is that if $x$ occurs free in $\varphi$ (e.g. $\varphi := (x=0)$) and $y$ is different from $x$, we have the equivalence :
As you can easily verify, if $x$ is free in $\varphi$, in the equivalent formula $x$ is bound and $y$ is free, that correspond to the fact that $x$ is disappeared and $y$ has taken its place.
What about the left conjunct ?
If $y$ is different from $x$, then $x=y$ is False and thus $x=y \to \varphi$ is True.
Conclusion :
as expected.
What happens when $y$ is the same as $x$ ? Clearly $(x=y \to \varphi) \leftrightarrow \varphi$ and also the right conjunct is $∃x(x=x ∧ \varphi) \leftrightarrow \varphi$.
The result is that $[y/x]\varphi \leftrightarrow \varphi$, again as expected, because if $y$ is the same of $x$ and $x$ is free in $\varphi$, the result of the operation of substitution of $y$ (i.e. $x$) in place of $x$ must be that the original formula is left unchanged.
Regarding (sb6),
Because if $x$ occurs free in $\varphi$, we want that $[x/x] \varphi$ is equivalent to $\varphi$, and $∀x(x=x → \varphi)$ is not, because $x$ is bound in it.