W&R's comment above is not clear to me.
According to logical rules, an abbreviation is only a "symbol": it cannot alter the theorems provable in the system.
Thus, if $x \ne y$ is (as usual) an abbreviation for $\lnot (x=y)$, we have no possibility of having different "sets of consequences".
I think that the comment is related to ✳13.19 : $\vdash ∃y(y=x)$, which is a correct logic rule, and to the "missing" semantics of PM.
In "modern" first-order logic, the law : $\vdash ∃y(y=x)$ is (universally) valid because we assume that every universe of discourse (i.e.every domain of interpretation) is not empty. Thus, in every interpretation, we have at least one object, which is for sure "equal to itself".
The above law is usually derived from the identity axiom : $x=x$ through the $\exists$-introduction rule :
from $\varphi(t)$, infer $\exists x \varphi(x)$.
If we apply the rule to $y \ne x$ (which is exactly : $\lnot (y=x)$), we can infer $∃y (y \ne x)$, but now we do not obtain a logical law.
The formula $∃y (y \ne x)$ is not (universally) valid because it is false in every domain with at least two objects, exactly like $y \ne x$.
I think that in ✳96.48 the free variable $w$ into $\sim(w=\overset{\smile}{R}‘max_R‘J_R‘x)$ must be read as implicitly universally quantified.
If so, the sub-formula is equivalent to $∀w \sim(w=\overset{\smile}{R}‘max_R‘J_R‘x)$ i.e.to $\sim \exists w (w=\overset{\smile}{R}‘max_R‘J_R‘x)$.
A possible reading of the annotation can be this: W&R want to avoid the misconception related to the above rule.
If we apply it to the formula $w\neq\overset{\smile}{R}‘max_R‘J_R‘x$ we can infer $\exists w (w\neq\overset{\smile}{R}‘max_R‘J_R‘x)$, which is not $\sim \exists w (w=\overset{\smile}{R}‘max_R‘J_R‘x)$.