Intuitionize fvelimab in iset.mm
Intuitionize fvelimab in iset.mm

This is a change of fvex to funfvex and the usual rearrangement of
the logic to establish that we are working within the domain of
the function. Also rename x,y to u,v throughout and add a variable
change at the end to avoid a distinct variable constraint
between A and x in the final theorem.

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