Fixes to conditional operator
Fixes to conditional operator

* Move the definition of the comma earlier in the file

* Remove discussion of weak deduction theorem. Even in set.mm
that's mostly an obsolete technique, and we're only adding if,
not the weak deduction theorem.

Accordingly, rename '"Weak deduction theorem" for set theory'
section to 'Conditional operator'.

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