The current definition of the value of a function at an argument (see df-fv) assures that this value is always a set, see fex. This is because this definition can be applied to any classes and , and evaluates to the empty set when it is not meaningful (as shown by ndmfv and fvprc).
Although it is very convenient for many theorems on functions and their proofs, there are some cases in which from alone it cannot be decided/derived whether is meaningful ( is actually a function which is defined for and really has the function value at ) or not. Therefore, additional assumptions are required, such as , or (see, for example, ndmfvrcl).
To avoid such an ambiguity, an alternative definition (see df-afv) would be possible which evaluates to the universal class () if it is not meaningful (see afvnfundmuv, ndmafv, afvprc and nfunsnafv), and which corresponds to the current definition () if it is (see afvfundmfveq). That means (see afvpcfv0), but is not generally valid.
In the theory of partial functions, it is a common case that is not defined at , which also would result in . In this context we say "is not defined" instead of "is not meaningful".
With this definition the following intuitive equivalence holds: <-> " is meaningful/defined".
An interesting question would be if could be replaced by in most of the theorems based on function values. If we look at the (currently 19) proofs using the definition df-fv of , we see that analogues for the following 8 theorems can be proven using the alternative definition: fveq1-> afveq1, fveq2-> afveq2, nffv-> nfafv, csbfv12-> csbafv12g , fvres-> afvres, rlimdm-> rlimdmafv, tz6.12-1-> tz6.12-1-afv, fveu-> afveu.
Three theorems proved by directly using df-fv are within a mathbox (fvsb) or not used (isumclim3, avril1).
However, the remaining 8 theorems proved by directly using df-fv are used more or less often:
* fvex: used in about 1750 proofs.
* tz6.12-1: root theorem of many theorems which have not a strict analogue, and which are used many times: fvprc (used in about 127 proofs), tz6.12i (used - indirectly via fvbr0 and fvrn0- in 18 proofs, and in fvclss used in fvclex used in fvresex, which is not used!), dcomex (used in 4 proofs), ndmfv (used in 86 proofs) and nfunsn (used by dffv2 which is not used).
* fv2: only used by elfv, which is only used by fv3, which is not used.
* dffv3: used by dffv4 (the previous "df-fv"), which now is only used in deprecated (usage discouraged) theorems or within mathboxes (csbfv12gALTVD), by shftval (itself used in 9 proofs), by dffv5 (mathbox) and by fvco2, which has the analogue afvco2.
* fvopab5: used only by ajval (not used) and by adjval (used - indirectly - in 9 proofs).
* zsum: used (via isum, sum0 and fsumsers) in more than 90 proofs.
* isumshft: used in pserdv2 and (via logtayl) 4 other proofs.
* ovtpos: used in 14 proofs.
As a result of this analysis we can say that the current definition of a function value is crucial for Metamath and cannot be exchanged easily with an alternative definition. While fv2, dffv3, fvopab5, zsum, isumshft and ovtpos are not critical or are, hopefully, also valid for the alternative definition, fvex and tz6.12-1 (and the theorems based on them) are essential for the current definition of function values.
With the same arguments, an alternative definition of operation values could be meaningful to avoid ambiguities, see df-aov.
For additional details, see https://groups.google.com/g/metamath/c/cteNUppB6A4.