Add operation equality theorems to iset.mm
Add operation equality theorems to iset.mm

This is fvoveq1d , fvoveq1 , ovanraleqv , and imbrov2fvoveq , copied
without change from set.mm.

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