Allow df-div to be used in the divfnzn proof
Allow df-div to be used in the divfnzn proof

I'm not sure why df-div is marked as discouraged (in set.mm),
but the proof of elq in set.mm uses it and I'm not sure how that
usage could easily be converted to divval (or anything else that
I've noticed). The way that elq in set.mm uses df-div is similar
to the way that divfnzn in iset.mm uses df-div.

metamath/set.mm,metamath/set.mm,metamath/set.mm