add sb8v; rename sb8*v -> sb8*f

[icecream17]

the previous sb8v is renamed sb8f, and sb8f's corresponding sb8v is made.

sb8ev and 2sb8ev are also renamed for consistency

The rename affects comments blindly

estimated axiom saves = 5:

sb8f: ax-10
abv: ax-10 ax-12
abvALT: ax-10 ax-12

[wlammen]

From a pure technical point I think here is hardly anything to discuss. This PR reduces dependencies on axioms, possibly with cascading effects on other theorems. The renaming here is the most critical point. I know from Norman Megill that he was keen to provide a stable database to the outside, maybe assuming there is scientific material elsewhere referencing the theorems by a link to web pages on metamath.com. If no one objects, I will merge this by tomorrow, though.