Explain why $d is used on its first use

set.mm

@@ -15580,8 +15580,28 @@ only postulated (that is, axiomatic) rule of inference of predicate
        This axiom essentially says that if ` x ` does not occur in ` ph ` ,
        i.e. ` ph ` does not depend on ` x ` in any way, then we can add the
        quantifier ` A. x ` to ` ph ` with no further assumptions.  By ~ sp , we
-       can also remove the quantifier (unconditionally).  (Contributed by NM,
-       10-Jan-1993.) $)
+       can also remove the quantifier (unconditionally).
+
+       This is our first use of a disjoint variable restriction aka distinct
+       variables ($d in the Metamath language).  It would be possible to
+       express our axioms without $d but there are good reasons we do it this
+       way.  The "obvious" way of truthfully expressing this axiom (and other
+       similar axioms) without distinct variable constraints ($d statements)
+       would lead to situations where even after the variable is done being
+       used you still can't discharge the distinctor.  This would mean its
+       logical equivalent would permanently stick around.  Effectively all
+       proofs would end up saying "provided there are at least N variables in
+       the metalogic, the following theorem holds" because you actually can't
+       prove anything about whether variables exist in this setting.  This
+       admits models where e.g. the object logic only has three variables v0 v1
+       v2 and so you can't write any expression containing four or more forall
+       or exists quantifiers without being degenerate in some way, so the
+       undischargeable assumptions that pile up are saying that the object
+       logic is at least nondegenerate enough to perform the proof in question.
+       The $d provisos provide a simple mechanism to eliminate the problem in
+       general.
+
+       (Contributed by NM, 10-Jan-1993.) $)
     ax-5 $a |- ( ph -> A. x ph ) $.
   $}