Add rspceeqv (#2811)
Add rspceeqv (#2811)

* add rspceeqv

* add the correct dv conditions to rspceeqv and minimize_with rspceeqv; 262 shortenings

* minor edits: 'complex-valued' and variants with a dash; deductive form-->deduction form; uniformization of some common phrases in comments; move 1red, 1cnd next to their variants

* remove backticks around a non-symbol in comment of rr2sscn2
metamath/set.mm,metamath/set.mm,metamath/set.mm