Yes, the issue is lack of Distinct Variables for Sets, Wffs and Classes, as introduced and described at MetaMath Proof Explorer.
If I understand correctly, the issue is lack of a type system that would separate the two categories at the axiom level.
