On 4/21/21 5:37 PM, Kyle Wyonch wrote:
I was wondering if this shortening [of cnfex] was valid
Short answer is, yes it is valid.
The longer answer is that set.mm defines a function evaluated outside
its domain to be the empty set which is why
http://us.metamath.org/mpeuni/fvex.html does not have any conditions.
By contrast, iset.mm does not have the ability to do quite this, so
instead cnfex would need to use
http://us.metamath.org/ileuni/funfvex.html or one of the other
alternatives under fvex at http://us.metamath.org/ileuni/mmil.html#setmm
There is some discussion of this in the "undefined results" section of
http://us.metamath.org/mpeuni/conventions.html and
http://us.metamath.org/ileuni/conventions.html
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/c36661f8-ac06-7264-2dd8-d95a1cb1b41f%40panix.com.
