Description: We now have prepared everything. The unwanted variable u is just in
one place left. pm2.61 can be used in conjunction with wl-ax11-lem9 to eliminate the second antecedent. Missing is something along the
lines of ax-6 , so we could remove the first antecedent. But the
Metamath axioms cannot accomplish this. Such a rule must reside one
abstraction level higher than all others: It says that a distinctor
implies a distinct variable condition on its contained setvar. This is
only needed if such conditions are required, as ax-11v does. The result
of this study is for me, that you cannot introduce a setvar capturing
this condition, and hope to eliminate it later. (Contributed by Wolf
Lammen, 30-Jun-2019)