Intuitionize elxp7 in iset.mm
Intuitionize elxp7 in iset.mm

This is just a matter of changing fvex to funfvex , together with
the observations that 1st and 2nd are each functions with domain
_V , and both sides of the equivalence imply A e. _V .

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