Difficulty understanding Metamath definitions of proper substitution. 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?
 A: 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 :

$[y/x]\varphi \leftrightarrow \exists x (x=y \land \varphi)$.

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 : 

$((x=y → \varphi) ∧ ∃x(x=y ∧ \varphi)) \leftrightarrow (\top \land ∃x(x=y ∧ \varphi)) \leftrightarrow ∃x(x=y ∧ \varphi)$,

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),

why $[x/x]ϕ ↔ ∀x(x=x → \varphi)$ would not hold ?

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.
