P. 478 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 47701-47800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	euoreqb 47701*	There is a set which is equal to one of two other sets iff the other sets are equal. (Contributed by AV, 24-Jan-2023.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (∃!𝑥 ∈ 𝑉 (𝑥 = 𝐴 ∨ 𝑥 = 𝐵) ↔ 𝐴 = 𝐵))
21.48.3.3  Analogs to Existential uniqueness (double quantification)
Theorem	2reu3 47702*	Double restricted existential uniqueness, analogous to 2eu3 2683. (Contributed by Alexander van der Vekens, 29-Jun-2017.)
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (∃*𝑥 ∈ 𝐴 𝜑 ∨ ∃*𝑦 ∈ 𝐵 𝜑) → ((∃!𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 𝜑 ∧ ∃!𝑦 ∈ 𝐵 ∃!𝑥 ∈ 𝐴 𝜑) ↔ (∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃!𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑)))
Theorem	2reu7 47703*	Two equivalent expressions for double restricted existential uniqueness, analogous to 2eu7 2687. (Contributed by Alexander van der Vekens, 2-Jul-2017.)
⊢ ((∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃!𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) ↔ ∃!𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑦 ∈ 𝐵 𝜑))
Theorem	2reu8 47704*	Two equivalent expressions for double restricted existential uniqueness, analogous to 2eu8 2688. Curiously, we can put ∃! on either of the internal conjuncts but not both. We can also commute ∃!𝑥 ∈ 𝐴∃!𝑦 ∈ 𝐵 using 2reu7 47703. (Contributed by Alexander van der Vekens, 2-Jul-2017.)
⊢ (∃!𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑦 ∈ 𝐵 𝜑) ↔ ∃!𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 (∃!𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑦 ∈ 𝐵 𝜑))
21.48.3.4  Additional theorems for double restricted existential uniqueness
Theorem	2reu8i 47705*	Implication of a double restricted existential uniqueness in terms of restricted existential quantification and restricted universal quantification, see also 2reu8 47704. The involved wffs depend on the setvar variables as follows: ph(x,y), ta(v,y), ch(x,w), th(v,w), et(x,b), ps(a,b), ze(a,w). (Contributed by AV, 1-Apr-2023.)
⊢ (𝑥 = 𝑣 → (𝜑 ↔ 𝜏))    &   ⊢ (𝑥 = 𝑣 → (𝜒 ↔ 𝜃))    &   ⊢ (𝑦 = 𝑤 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑦 = 𝑏 → (𝜑 ↔ 𝜂))    &   ⊢ (𝑥 = 𝑎 → (𝜒 ↔ 𝜁))    &   ⊢ (((𝜒 → 𝑦 = 𝑤) ∧ 𝜁) → 𝑦 = 𝑤)    &   ⊢ ((𝑥 = 𝑎 ∧ 𝑦 = 𝑏) → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃!𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜂 → (𝑏 = 𝑦 ∧ (𝜓 → 𝑎 = 𝑥)))))
Theorem	2reuimp0 47706*	Implication of a double restricted existential uniqueness in terms of restricted existential quantification and restricted universal quantification. The involved wffs depend on the setvar variables as follows: ph(a,b), th(a,c), ch(d,b), ta(d,c), et(a,e), ps(a,f) (Contributed by AV, 13-Mar-2023.)
⊢ (𝑏 = 𝑐 → (𝜑 ↔ 𝜃))    &   ⊢ (𝑎 = 𝑑 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑎 = 𝑑 → (𝜃 ↔ 𝜏))    &   ⊢ (𝑏 = 𝑒 → (𝜑 ↔ 𝜂))    &   ⊢ (𝑐 = 𝑓 → (𝜃 ↔ 𝜓))    ⇒   ⊢ (∃!𝑎 ∈ 𝑉 ∃!𝑏 ∈ 𝑉 𝜑 → ∃𝑎 ∈ 𝑉 ∀𝑑 ∈ 𝑉 ∀𝑏 ∈ 𝑉 ∃𝑒 ∈ 𝑉 ∀𝑓 ∈ 𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓 → 𝑒 = 𝑓)))
Theorem	2reuimp 47707*	Implication of a double restricted existential uniqueness in terms of restricted existential quantification and restricted universal quantification if the class of the quantified elements is not empty. (Contributed by AV, 13-Mar-2023.)
⊢ (𝑏 = 𝑐 → (𝜑 ↔ 𝜃))    &   ⊢ (𝑎 = 𝑑 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑎 = 𝑑 → (𝜃 ↔ 𝜏))    &   ⊢ (𝑏 = 𝑒 → (𝜑 ↔ 𝜂))    &   ⊢ (𝑐 = 𝑓 → (𝜃 ↔ 𝜓))    ⇒   ⊢ ((𝑉 ≠ ∅ ∧ ∃!𝑎 ∈ 𝑉 ∃!𝑏 ∈ 𝑉 𝜑) → ∃𝑎 ∈ 𝑉 ∀𝑑 ∈ 𝑉 ∀𝑏 ∈ 𝑉 ∃𝑒 ∈ 𝑉 ∀𝑓 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ((𝜒 ∧ (𝜏 → 𝑏 = 𝑐)) → (𝜓 → (𝜂 ∧ (𝑎 = 𝑑 ∧ 𝑒 = 𝑓)))))
21.48.4  Alternative definitions of function and operation values The current definition of the value (𝐹‘𝐴) of a function 𝐹 at an argument 𝐴 (see df-fv 6533) assures that this value is always a set, see fex 7214. 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 6903 and fvprc 6863). 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 ∅ ∉ ran 𝐹, ∅ ∈ ran 𝐹 or Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹 (see, for example, ndmfvrcl 6904). To avoid such an ambiguity, an alternative definition (𝐹'''𝐴) (see df-afv 47712) would be possible which evaluates to the universal class ((𝐹'''𝐴) = V) if it is not meaningful (see afvnfundmuv 47731, ndmafv 47732, afvprc 47736 and nfunsnafv 47734), and which corresponds to the current definition ((𝐹‘𝐴) = (𝐹'''𝐴)) if it is (see afvfundmfveq 47730). That means (𝐹'''𝐴) = V → (𝐹‘𝐴) = ∅ (see afvpcfv0 47738), but (𝐹‘𝐴) = ∅ → (𝐹'''𝐴) = V 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 (𝐹'''𝐴) = V. In this context we say (𝐹'''𝐴) "is not defined" instead of "is not meaningful". With this definition the following intuitive equivalence holds: (𝐹'''𝐴) ∈ V <-> "(𝐹'''𝐴) 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 6533 of (𝐹‘𝐴), we see that analogues for the following 8 theorems can be proven using the alternative definition: fveq1 6870-> afveq1 47726, fveq2 6871-> afveq2 47727, nffv 6881-> nfafv 47728, csbfv12 6916-> csbafv12g , fvres 6890-> afvres 47764, rlimdm 15592-> rlimdmafv 47769, tz6.12-1 6894-> tz6.12-1-afv 47766, fveu 6860-> afveu 47745. Three theorems proved by directly using df-fv 6533 are within a mathbox (fvsb 45025) or not used (isumclim3 15800, avril1 30723). However, the remaining 8 theorems proved by directly using df-fv 6533 are used more or less often: * fvex 6884: used in about 1750 proofs. * tz6.12-1 6894: root theorem of many theorems which have not a strict analogue, and which are used many times: fvprc 6863 (used in about 127 proofs), tz6.12i 6897 (used - indirectly via fvbr0 6898 and fvrn0 6899- in 18 proofs, and in fvclss 7229 used in fvclex 7944 used in fvresex 7945, which is not used!), dcomex 10419 (used in 4 proofs), ndmfv 6903 (used in 86 proofs) and nfunsn 6910 (used by dffv2 6966 which is not used). * fv2 6866: only used by elfv 6869, which is only used by fv3 6889, which is not used. * dffv3 6867: used by dffv4 6868 (the previous "df-fv"), which now is only used in deprecated (usage discouraged) theorems or within mathboxes (csbfv12gALTVD 45472), by shftval 15101 (itself used in 9 proofs), by dffv5 36285 (mathbox) and by fvco2 6968, which has the analogue afvco2 47768. * fvopab5 7013: used only by ajval 31122 (not used) and by adjval 32151 (used - indirectly - in 9 proofs). * zsum 15759: used (via isum 15760, sum0 15762 and fsumsers 15769) in more than 90 proofs. * isumshft 15883: used in pserdv2 26551 and (via logtayl 26783) 4 other proofs. * ovtpos 8225: 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 6866, dffv3 6867, fvopab5 7013, zsum 15759, isumshft 15883 and ovtpos 8225 are not critical or are, hopefully, also valid for the alternative definition, fvex 6884 and tz6.12-1 6894 (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 47713. For additional details, see https://groups.google.com/g/metamath/c/cteNUppB6A4 47713.
Syntax	wdfat 47708	Extend the definition of a wff to include the "defined at" predicate. Read: "(the function) 𝐹 is defined at (the argument) 𝐴". In a previous version, the token "def@" was used. However, since the @ is used (informally) as a replacement for $ in commented out sections that may be deleted some day. While there is no violation of any standard to use the @ in a token, it could make the search for such commented-out sections slightly more difficult. (See remark of Norman Megill at https://groups.google.com/g/metamath/c/cteNUppB6A4).
wff 𝐹 defAt 𝐴
Syntax	cafv 47709	Extend the definition of a class to include the value of a function. Read: "the value of 𝐹 at 𝐴 " or "𝐹 of 𝐴". In a previous version, the symbol " ' " was used. However, since the similarity with the symbol ‘ used for the current definition of a function's value (see df-fv 6533), which, by the way, was intended to visualize that in many cases ‘ and " ' " are exchangeable, makes reading the theorems, especially those which use both definitions as dfafv2 47724, very difficult, 3 apostrophes ''' are used now so that it's easier to distinguish from df-fv 6533 and df-ima 5665. And not three backticks ( three times ‘) since that would be annoying to escape in a comment. (See remark of Norman Megill and Gerard Lang at https://groups.google.com/g/metamath/c/cteNUppB6A4 5665).
class (𝐹'''𝐴)
Syntax	caov 47710	Extend class notation to include the value of an operation 𝐹 (such as +) for two arguments 𝐴 and 𝐵. Note that the syntax is simply three class symbols in a row surrounded by a pair of parentheses in contrast to the current definition, see df-ov 7403.
class ((𝐴𝐹𝐵))
Definition	df-dfat 47711	Definition of the predicate that determines if some class 𝐹 is defined as function for an argument 𝐴 or, in other words, if the function value for some class 𝐹 for an argument 𝐴 is defined. We say that 𝐹 is defined at 𝐴 if a 𝐹 is a function restricted to the member 𝐴 of its domain. (Contributed by Alexander van der Vekens, 25-May-2017.)
⊢ (𝐹 defAt 𝐴 ↔ (𝐴 ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {𝐴})))
Definition	df-afv 47712*	Alternative definition of the value of a function, (𝐹'''𝐴), also known as function application. In contrast to (𝐹‘𝐴) = ∅ (see df-fv 6533 and ndmfv 6903), (𝐹'''𝐴) = V if F is not defined for A! (Contributed by Alexander van der Vekens, 25-May-2017.) (Revised by BJ/AV, 25-Aug-2022.)
⊢ (𝐹'''𝐴) = (℩'𝑥𝐴𝐹𝑥)
Definition	df-aov 47713	Define the value of an operation. In contrast to df-ov 7403, the alternative definition for a function value (see df-afv 47712) is used. By this, the value of the operation applied to two arguments is the universal class if the operation is not defined for these two arguments. There are still no restrictions of any kind on what those class expressions may be, although only certain kinds of class expressions - a binary operation 𝐹 and its arguments 𝐴 and 𝐵- will be useful for proving meaningful theorems. (Contributed by Alexander van der Vekens, 26-May-2017.)
⊢ ((𝐴𝐹𝐵)) = (𝐹'''⟨𝐴, 𝐵⟩)
21.48.4.1  Restricted quantification (extension)
Theorem	ralbinrald 47714*	Elemination of a restricted universal quantification under certain conditions. (Contributed by Alexander van der Vekens, 2-Aug-2017.)
⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝑥 ∈ 𝐴 → 𝑥 = 𝑋)    &   ⊢ (𝑥 = 𝑋 → (𝜓 ↔ 𝜃))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ 𝜃))
21.48.4.2  The universal class (extension)
Theorem	nvelim 47715	If a class is the universal class it doesn't belong to any class, generalization of nvel 5274. (Contributed by Alexander van der Vekens, 26-May-2017.)
⊢ (𝐴 = V → ¬ 𝐴 ∈ 𝐵)
21.48.4.3  Introduce the Axiom of Power Sets (extension)
Theorem	alneu 47716	If a statement holds for all sets, there is not a unique set for which the statement holds. (Contributed by Alexander van der Vekens, 28-Nov-2017.)
⊢ (∀𝑥𝜑 → ¬ ∃!𝑥𝜑)
Theorem	eu2ndop1stv 47717*	If there is a unique second component in an ordered pair contained in a given set, the first component must be a set. (Contributed by Alexander van der Vekens, 29-Nov-2017.)
⊢ (∃!𝑦⟨𝐴, 𝑦⟩ ∈ 𝑉 → 𝐴 ∈ V)
21.48.4.4  Predicate "defined at"
Theorem	dfateq12d 47718	Equality deduction for "defined at". (Contributed by Alexander van der Vekens, 26-May-2017.)
⊢ (𝜑 → 𝐹 = 𝐺)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐹 defAt 𝐴 ↔ 𝐺 defAt 𝐵))
Theorem	nfdfat 47719	Bound-variable hypothesis builder for "defined at". To prove a deduction version of this theorem is not easily possible because many deduction versions for bound-variable hypothesis builder for constructs the definition of "defined at" is based on are not available (e.g., for Fun/Rel, dom, ⊆, etc.). (Contributed by Alexander van der Vekens, 26-May-2017.)
⊢ Ⅎ𝑥𝐹    &   ⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥 𝐹 defAt 𝐴
Theorem	dfdfat2 47720*	Alternate definition of the predicate "defined at" not using the Fun predicate. (Contributed by Alexander van der Vekens, 22-Jul-2017.) (Proof shortened by Peter Mazsa, 2-Oct-2022.)
⊢ (𝐹 defAt 𝐴 ↔ (𝐴 ∈ dom 𝐹 ∧ ∃!𝑦 𝐴𝐹𝑦))
Theorem	fundmdfat 47721	A function is defined at any element of its domain. (Contributed by AV, 2-Sep-2022.)
⊢ ((Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹) → 𝐹 defAt 𝐴)
Theorem	dfatprc 47722	A function is not defined at a proper class. (Contributed by AV, 1-Sep-2022.)
⊢ (¬ 𝐴 ∈ V → ¬ 𝐹 defAt 𝐴)
Theorem	dfatelrn 47723	The value of a function 𝐹 at a set 𝐴 is in the range of the function 𝐹 if 𝐹 is defined at 𝐴. (Contributed by AV, 1-Sep-2022.)
⊢ (𝐹 defAt 𝐴 → (𝐹‘𝐴) ∈ ran 𝐹)
21.48.4.5  Alternative definition of the value of a function
Theorem	dfafv2 47724	Alternative definition of (𝐹'''𝐴) using (𝐹‘𝐴) directly. (Contributed by Alexander van der Vekens, 22-Jul-2017.) (Revised by AV, 25-Aug-2022.)
⊢ (𝐹'''𝐴) = if(𝐹 defAt 𝐴, (𝐹‘𝐴), V)
Theorem	afveq12d 47725	Equality deduction for function value, analogous to fveq12d 6878. (Contributed by Alexander van der Vekens, 26-May-2017.)
⊢ (𝜑 → 𝐹 = 𝐺)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐹'''𝐴) = (𝐺'''𝐵))
Theorem	afveq1 47726	Equality theorem for function value, analogous to fveq1 6870. (Contributed by Alexander van der Vekens, 22-Jul-2017.)
⊢ (𝐹 = 𝐺 → (𝐹'''𝐴) = (𝐺'''𝐴))
Theorem	afveq2 47727	Equality theorem for function value, analogous to fveq1 6870. (Contributed by Alexander van der Vekens, 22-Jul-2017.)
⊢ (𝐴 = 𝐵 → (𝐹'''𝐴) = (𝐹'''𝐵))
Theorem	nfafv 47728	Bound-variable hypothesis builder for function value, analogous to nffv 6881. To prove a deduction version of this analogous to nffvd 6883 is not easily possible because a deduction version of nfdfat 47719 cannot be shown easily. (Contributed by Alexander van der Vekens, 26-May-2017.)
⊢ Ⅎ𝑥𝐹    &   ⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥(𝐹'''𝐴)
Theorem	csbafv12g 47729	Move class substitution in and out of a function value, analogous to csbfv12 6916, with a direct proof proposed by Mario Carneiro, analogous to csbov123 7444. (Contributed by Alexander van der Vekens, 23-Jul-2017.)
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌(𝐹'''𝐵) = (⦋𝐴 / 𝑥⦌𝐹'''⦋𝐴 / 𝑥⦌𝐵))
Theorem	afvfundmfveq 47730	If a class is a function restricted to a member of its domain, then the function value for this member is equal for both definitions. (Contributed by Alexander van der Vekens, 25-May-2017.)
⊢ (𝐹 defAt 𝐴 → (𝐹'''𝐴) = (𝐹‘𝐴))
Theorem	afvnfundmuv 47731	If a set is not in the domain of a class or the class is not a function restricted to the set, then the function value for this set is the universe. (Contributed by Alexander van der Vekens, 26-May-2017.)
⊢ (¬ 𝐹 defAt 𝐴 → (𝐹'''𝐴) = V)
Theorem	ndmafv 47732	The value of a class outside its domain is the universe, compare with ndmfv 6903. (Contributed by Alexander van der Vekens, 25-May-2017.)
⊢ (¬ 𝐴 ∈ dom 𝐹 → (𝐹'''𝐴) = V)
Theorem	afvvdm 47733	If the function value of a class for an argument is a set, the argument is contained in the domain of the class. (Contributed by Alexander van der Vekens, 25-May-2017.)
⊢ ((𝐹'''𝐴) ∈ 𝐵 → 𝐴 ∈ dom 𝐹)
Theorem	nfunsnafv 47734	If the restriction of a class to a singleton is not a function, its value is the universe, compare with nfunsn 6910. (Contributed by Alexander van der Vekens, 25-May-2017.)
⊢ (¬ Fun (𝐹 ↾ {𝐴}) → (𝐹'''𝐴) = V)
Theorem	afvvfunressn 47735	If the function value of a class for an argument is a set, the class restricted to the singleton of the argument is a function. (Contributed by Alexander van der Vekens, 25-May-2017.)
⊢ ((𝐹'''𝐴) ∈ 𝐵 → Fun (𝐹 ↾ {𝐴}))
Theorem	afvprc 47736	A function's value at a proper class is the universe, compare with fvprc 6863. (Contributed by Alexander van der Vekens, 25-May-2017.)
⊢ (¬ 𝐴 ∈ V → (𝐹'''𝐴) = V)
Theorem	afvvv 47737	If a function's value at an argument is a set, the argument is also a set. (Contributed by Alexander van der Vekens, 25-May-2017.)
⊢ ((𝐹'''𝐴) ∈ 𝐵 → 𝐴 ∈ V)
Theorem	afvpcfv0 47738	If the value of the alternative function at an argument is the universe, the function's value at this argument is the empty set. (Contributed by Alexander van der Vekens, 25-May-2017.)
⊢ ((𝐹'''𝐴) = V → (𝐹‘𝐴) = ∅)
Theorem	afvnufveq 47739	The value of the alternative function at a set as argument equals the function's value at this argument. (Contributed by Alexander van der Vekens, 25-May-2017.)
⊢ ((𝐹'''𝐴) ≠ V → (𝐹'''𝐴) = (𝐹‘𝐴))
Theorem	afvvfveq 47740	The value of the alternative function at a set as argument equals the function's value at this argument. (Contributed by Alexander van der Vekens, 25-May-2017.)
⊢ ((𝐹'''𝐴) ∈ 𝐵 → (𝐹'''𝐴) = (𝐹‘𝐴))
Theorem	afv0fv0 47741	If the value of the alternative function at an argument is the empty set, the function's value at this argument is the empty set. (Contributed by Alexander van der Vekens, 25-May-2017.)
⊢ ((𝐹'''𝐴) = ∅ → (𝐹‘𝐴) = ∅)
Theorem	afvfvn0fveq 47742	If the function's value at an argument is not the empty set, it equals the value of the alternative function at this argument. (Contributed by Alexander van der Vekens, 25-May-2017.)
⊢ ((𝐹‘𝐴) ≠ ∅ → (𝐹'''𝐴) = (𝐹‘𝐴))
Theorem	afv0nbfvbi 47743	The function's value at an argument is an element of a set if and only if the value of the alternative function at this argument is an element of that set, if the set does not contain the empty set. (Contributed by Alexander van der Vekens, 25-May-2017.)
⊢ (∅ ∉ 𝐵 → ((𝐹'''𝐴) ∈ 𝐵 ↔ (𝐹‘𝐴) ∈ 𝐵))
Theorem	afvfv0bi 47744	The function's value at an argument is the empty set if and only if the value of the alternative function at this argument is either the empty set or the universe. (Contributed by Alexander van der Vekens, 25-May-2017.)
⊢ ((𝐹‘𝐴) = ∅ ↔ ((𝐹'''𝐴) = ∅ ∨ (𝐹'''𝐴) = V))
Theorem	afveu 47745*	The value of a function at a unique point, analogous to fveu 6860. (Contributed by Alexander van der Vekens, 29-Nov-2017.)
⊢ (∃!𝑥 𝐴𝐹𝑥 → (𝐹'''𝐴) = ∪ {𝑥 ∣ 𝐴𝐹𝑥})
Theorem	fnbrafvb 47746	Equivalence of function value and binary relation, analogous to fnbrfvb 6921. (Contributed by Alexander van der Vekens, 25-May-2017.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → ((𝐹'''𝐵) = 𝐶 ↔ 𝐵𝐹𝐶))
Theorem	fnopafvb 47747	Equivalence of function value and ordered pair membership, analogous to fnopfvb 6922. (Contributed by Alexander van der Vekens, 25-May-2017.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → ((𝐹'''𝐵) = 𝐶 ↔ ⟨𝐵, 𝐶⟩ ∈ 𝐹))
Theorem	funbrafvb 47748	Equivalence of function value and binary relation, analogous to funbrfvb 6924. (Contributed by Alexander van der Vekens, 25-May-2017.)
⊢ ((Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹) → ((𝐹'''𝐴) = 𝐵 ↔ 𝐴𝐹𝐵))
Theorem	funopafvb 47749	Equivalence of function value and ordered pair membership, analogous to funopfvb 6925. (Contributed by Alexander van der Vekens, 25-May-2017.)
⊢ ((Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹) → ((𝐹'''𝐴) = 𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝐹))
Theorem	funbrafv 47750	The second argument of a binary relation on a function is the function's value, analogous to funbrfv 6919. (Contributed by Alexander van der Vekens, 25-May-2017.)
⊢ (Fun 𝐹 → (𝐴𝐹𝐵 → (𝐹'''𝐴) = 𝐵))
Theorem	funbrafv2b 47751	Function value in terms of a binary relation, analogous to funbrfv2b 6928. (Contributed by Alexander van der Vekens, 25-May-2017.)
⊢ (Fun 𝐹 → (𝐴𝐹𝐵 ↔ (𝐴 ∈ dom 𝐹 ∧ (𝐹'''𝐴) = 𝐵)))
Theorem	dfafn5a 47752*	Representation of a function in terms of its values, analogous to dffn5 6929 (only one direction of implication!). (Contributed by Alexander van der Vekens, 25-May-2017.)
⊢ (𝐹 Fn 𝐴 → 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹'''𝑥)))
Theorem	dfafn5b 47753*	Representation of a function in terms of its values, analogous to dffn5 6929 (only if it is assumed that the function value for each x is a set). (Contributed by Alexander van der Vekens, 25-May-2017.)
⊢ (∀𝑥 ∈ 𝐴 (𝐹'''𝑥) ∈ 𝑉 → (𝐹 Fn 𝐴 ↔ 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹'''𝑥))))
Theorem	fnrnafv 47754*	The range of a function expressed as a collection of the function's values, analogous to fnrnfv 6930. (Contributed by Alexander van der Vekens, 25-May-2017.)
⊢ (𝐹 Fn 𝐴 → ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹'''𝑥)})
Theorem	afvelrnb 47755*	A member of a function's range is a value of the function, analogous to fvelrnb 6931 with the additional requirement that the member must be a set. (Contributed by Alexander van der Vekens, 25-May-2017.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝑉) → (𝐵 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 (𝐹'''𝑥) = 𝐵))
Theorem	afvelrnb0 47756*	A member of a function's range is a value of the function, only one direction of implication of fvelrnb 6931. (Contributed by Alexander van der Vekens, 1-Jun-2017.)
⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ ran 𝐹 → ∃𝑥 ∈ 𝐴 (𝐹'''𝑥) = 𝐵))
Theorem	dfaimafn 47757*	Alternate definition of the image of a function, analogous to dfimafn 6933. (Contributed by Alexander van der Vekens, 25-May-2017.)
⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹) → (𝐹 “ 𝐴) = {𝑦 ∣ ∃𝑥 ∈ 𝐴 (𝐹'''𝑥) = 𝑦})
Theorem	dfaimafn2 47758*	Alternate definition of the image of a function as an indexed union of singletons of function values, analogous to dfimafn2 6934. (Contributed by Alexander van der Vekens, 25-May-2017.)
⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹) → (𝐹 “ 𝐴) = ∪ 𝑥 ∈ 𝐴 {(𝐹'''𝑥)})
Theorem	afvelima 47759*	Function value in an image, analogous to fvelima 6936. (Contributed by Alexander van der Vekens, 25-May-2017.)
⊢ ((Fun 𝐹 ∧ 𝐴 ∈ (𝐹 “ 𝐵)) → ∃𝑥 ∈ 𝐵 (𝐹'''𝑥) = 𝐴)
Theorem	afvelrn 47760	A function's value belongs to its range, analogous to fvelrn 7061. (Contributed by Alexander van der Vekens, 25-May-2017.)
⊢ ((Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹) → (𝐹'''𝐴) ∈ ran 𝐹)
Theorem	fnafvelrn 47761	A function's value belongs to its range, analogous to fnfvelrn 7065. (Contributed by Alexander van der Vekens, 25-May-2017.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → (𝐹'''𝐵) ∈ ran 𝐹)
Theorem	fafvelcdm 47762	A function's value belongs to its codomain, analogous to ffvelcdm 7066. (Contributed by Alexander van der Vekens, 25-May-2017.)
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → (𝐹'''𝐶) ∈ 𝐵)
Theorem	ffnafv 47763*	A function maps to a class to which all values belong, analogous to ffnfv 7104. (Contributed by Alexander van der Vekens, 25-May-2017.)
⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹'''𝑥) ∈ 𝐵))
Theorem	afvres 47764	The value of a restricted function, analogous to fvres 6890. (Contributed by Alexander van der Vekens, 22-Jul-2017.)
⊢ (𝐴 ∈ 𝐵 → ((𝐹 ↾ 𝐵)'''𝐴) = (𝐹'''𝐴))
Theorem	tz6.12-afv 47765*	Function value. Theorem 6.12(1) of [TakeutiZaring] p. 27, analogous to tz6.12 6895. (Contributed by Alexander van der Vekens, 29-Nov-2017.)
⊢ ((⟨𝐴, 𝑦⟩ ∈ 𝐹 ∧ ∃!𝑦⟨𝐴, 𝑦⟩ ∈ 𝐹) → (𝐹'''𝐴) = 𝑦)
Theorem	tz6.12-1-afv 47766*	Function value (Theorem 6.12(1) of [TakeutiZaring] p. 27, analogous to tz6.12-1 6894. (Contributed by Alexander van der Vekens, 29-Nov-2017.)
⊢ ((𝐴𝐹𝑦 ∧ ∃!𝑦 𝐴𝐹𝑦) → (𝐹'''𝐴) = 𝑦)
Theorem	dmfcoafv 47767	Domains of a function composition, analogous to dmfco 6967. (Contributed by Alexander van der Vekens, 23-Jul-2017.)
⊢ ((Fun 𝐺 ∧ 𝐴 ∈ dom 𝐺) → (𝐴 ∈ dom (𝐹 ∘ 𝐺) ↔ (𝐺'''𝐴) ∈ dom 𝐹))
Theorem	afvco2 47768	Value of a function composition, analogous to fvco2 6968. (Contributed by Alexander van der Vekens, 23-Jul-2017.)
⊢ ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → ((𝐹 ∘ 𝐺)'''𝑋) = (𝐹'''(𝐺'''𝑋)))
Theorem	rlimdmafv 47769	Two ways to express that a function has a limit, analogous to rlimdm 15592. (Contributed by Alexander van der Vekens, 27-Nov-2017.)
⊢ (𝜑 → 𝐹:𝐴⟶ℂ)    &   ⊢ (𝜑 → sup(𝐴, ℝ*, < ) = +∞)    ⇒   ⊢ (𝜑 → (𝐹 ∈ dom ⇝𝑟 ↔ 𝐹 ⇝𝑟 ( ⇝𝑟 '''𝐹)))
21.48.4.6  Alternative definition of the value of an operation
Theorem	aoveq123d 47770	Equality deduction for operation value, analogous to oveq123d 7421. (Contributed by Alexander van der Vekens, 26-May-2017.)
⊢ (𝜑 → 𝐹 = 𝐺)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → ((𝐴𝐹𝐶)) = ((𝐵𝐺𝐷)) )
Theorem	nfaov 47771	Bound-variable hypothesis builder for operation value, analogous to nfov 7430. To prove a deduction version of this analogous to nfovd 7429 is not quickly possible because many deduction versions for bound-variable hypothesis builder for constructs the definition of alternative operation values is based on are not available (see nfafv 47728). (Contributed by Alexander van der Vekens, 26-May-2017.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐹    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥 ((𝐴𝐹𝐵))
Theorem	csbaovg 47772	Move class substitution in and out of an operation. (Contributed by Alexander van der Vekens, 26-May-2017.)
⊢ (𝐴 ∈ 𝐷 → ⦋𝐴 / 𝑥⦌ ((𝐵𝐹𝐶)) = ((⦋𝐴 / 𝑥⦌𝐵⦋𝐴 / 𝑥⦌𝐹⦋𝐴 / 𝑥⦌𝐶)) )
Theorem	aovfundmoveq 47773	If a class is a function restricted to an ordered pair of its domain, then the value of the operation on this pair is equal for both definitions. (Contributed by Alexander van der Vekens, 26-May-2017.)
⊢ (𝐹 defAt ⟨𝐴, 𝐵⟩ → ((𝐴𝐹𝐵)) = (𝐴𝐹𝐵))
Theorem	aovnfundmuv 47774	If an ordered pair is not in the domain of a class or the class is not a function restricted to the ordered pair, then the operation value for this pair is the universal class. (Contributed by Alexander van der Vekens, 26-May-2017.)
⊢ (¬ 𝐹 defAt ⟨𝐴, 𝐵⟩ → ((𝐴𝐹𝐵)) = V)
Theorem	ndmaov 47775	The value of an operation outside its domain, analogous to ndmafv 47732. (Contributed by Alexander van der Vekens, 26-May-2017.)
⊢ (¬ ⟨𝐴, 𝐵⟩ ∈ dom 𝐹 → ((𝐴𝐹𝐵)) = V)
Theorem	ndmaovg 47776	The value of an operation outside its domain, analogous to ndmovg 7583. (Contributed by Alexander van der Vekens, 26-May-2017.)
⊢ ((dom 𝐹 = (𝑅 × 𝑆) ∧ ¬ (𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆)) → ((𝐴𝐹𝐵)) = V)
Theorem	aovvdm 47777	If the operation value of a class for an ordered pair is a set, the ordered pair is contained in the domain of the class. (Contributed by Alexander van der Vekens, 26-May-2017.)
⊢ ( ((𝐴𝐹𝐵)) ∈ 𝐶 → ⟨𝐴, 𝐵⟩ ∈ dom 𝐹)
Theorem	nfunsnaov 47778	If the restriction of a class to a singleton is not a function, its operation value is the universal class. (Contributed by Alexander van der Vekens, 26-May-2017.)
⊢ (¬ Fun (𝐹 ↾ {⟨𝐴, 𝐵⟩}) → ((𝐴𝐹𝐵)) = V)
Theorem	aovvfunressn 47779	If the operation value of a class for an argument is a set, the class restricted to the singleton of the argument is a function. (Contributed by Alexander van der Vekens, 26-May-2017.)
⊢ ( ((𝐴𝐹𝐵)) ∈ 𝐶 → Fun (𝐹 ↾ {⟨𝐴, 𝐵⟩}))
Theorem	aovprc 47780	The value of an operation when the one of the arguments is a proper class, analogous to ovprc 7438. (Contributed by Alexander van der Vekens, 26-May-2017.)
⊢ Rel dom 𝐹    ⇒   ⊢ (¬ (𝐴 ∈ V ∧ 𝐵 ∈ V) → ((𝐴𝐹𝐵)) = V)
Theorem	aovrcl 47781	Reverse closure for an operation value, analogous to afvvv 47737. In contrast to ovrcl 7441, elementhood of the operation's value in a set is required, not containing an element. (Contributed by Alexander van der Vekens, 26-May-2017.)
⊢ Rel dom 𝐹    ⇒   ⊢ ( ((𝐴𝐹𝐵)) ∈ 𝐶 → (𝐴 ∈ V ∧ 𝐵 ∈ V))
Theorem	aovpcov0 47782	If the alternative value of the operation on an ordered pair is the universal class, the operation's value at this ordered pair is the empty set. (Contributed by Alexander van der Vekens, 26-May-2017.)
⊢ ( ((𝐴𝐹𝐵)) = V → (𝐴𝐹𝐵) = ∅)
Theorem	aovnuoveq 47783	The alternative value of the operation on an ordered pair equals the operation's value at this ordered pair. (Contributed by Alexander van der Vekens, 26-May-2017.)
⊢ ( ((𝐴𝐹𝐵)) ≠ V → ((𝐴𝐹𝐵)) = (𝐴𝐹𝐵))
Theorem	aovvoveq 47784	The alternative value of the operation on an ordered pair equals the operation's value on this ordered pair. (Contributed by Alexander van der Vekens, 26-May-2017.)
⊢ ( ((𝐴𝐹𝐵)) ∈ 𝐶 → ((𝐴𝐹𝐵)) = (𝐴𝐹𝐵))
Theorem	aov0ov0 47785	If the alternative value of the operation on an ordered pair is the empty set, the operation's value at this ordered pair is the empty set. (Contributed by Alexander van der Vekens, 26-May-2017.)
⊢ ( ((𝐴𝐹𝐵)) = ∅ → (𝐴𝐹𝐵) = ∅)
Theorem	aovovn0oveq 47786	If the operation's value at an argument is not the empty set, it equals the value of the alternative operation at this argument. (Contributed by Alexander van der Vekens, 26-May-2017.)
⊢ ((𝐴𝐹𝐵) ≠ ∅ → ((𝐴𝐹𝐵)) = (𝐴𝐹𝐵))
Theorem	aov0nbovbi 47787	The operation's value on an ordered pair is an element of a set if and only if the alternative value of the operation on this ordered pair is an element of that set, if the set does not contain the empty set. (Contributed by Alexander van der Vekens, 26-May-2017.)
⊢ (∅ ∉ 𝐶 → ( ((𝐴𝐹𝐵)) ∈ 𝐶 ↔ (𝐴𝐹𝐵) ∈ 𝐶))
Theorem	aovov0bi 47788	The operation's value on an ordered pair is the empty set if and only if the alternative value of the operation on this ordered pair is either the empty set or the universal class. (Contributed by Alexander van der Vekens, 26-May-2017.)
⊢ ((𝐴𝐹𝐵) = ∅ ↔ ( ((𝐴𝐹𝐵)) = ∅ ∨ ((𝐴𝐹𝐵)) = V))
Theorem	rspceaov 47789*	A frequently used special case of rspc2ev 3597 for operation values, analogous to rspceov 7449. (Contributed by Alexander van der Vekens, 26-May-2017.)
⊢ ((𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ∧ 𝑆 = ((𝐶𝐹𝐷)) ) → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑆 = ((𝑥𝐹𝑦)) )
Theorem	fnotaovb 47790	Equivalence of operation value and ordered triple membership, analogous to fnopfvb 6922. (Contributed by Alexander van der Vekens, 26-May-2017.)
⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵) → ( ((𝐶𝐹𝐷)) = 𝑅 ↔ ⟨𝐶, 𝐷, 𝑅⟩ ∈ 𝐹))
Theorem	ffnaov 47791*	An operation maps to a class to which all values belong, analogous to ffnov 7526. (Contributed by Alexander van der Vekens, 26-May-2017.)
⊢ (𝐹:(𝐴 × 𝐵)⟶𝐶 ↔ (𝐹 Fn (𝐴 × 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ((𝑥𝐹𝑦)) ∈ 𝐶))
Theorem	faovcl 47792	Closure law for an operation, analogous to fovcl 7528. (Contributed by Alexander van der Vekens, 26-May-2017.)
⊢ 𝐹:(𝑅 × 𝑆)⟶𝐶    ⇒   ⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) → ((𝐴𝐹𝐵)) ∈ 𝐶)
Theorem	aovmpt4g 47793*	Value of a function given by the maps-to notation, analogous to ovmpt4g 7547. (Contributed by Alexander van der Vekens, 26-May-2017.)
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)    ⇒   ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉) → ((𝑥𝐹𝑦)) = 𝐶)
Theorem	aoprssdm 47794*	Domain of closure of an operation. In contrast to oprssdm 7581, no additional property for S (¬ ∅ ∈ 𝑆) is required! (Contributed by Alexander van der Vekens, 26-May-2017.)
⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → ((𝑥𝐹𝑦)) ∈ 𝑆)    ⇒   ⊢ (𝑆 × 𝑆) ⊆ dom 𝐹
Theorem	ndmaovcl 47795	The "closure" of an operation outside its domain, when the operation's value is a set in contrast to ndmovcl 7585 where it is required that the domain contains the empty set (∅ ∈ 𝑆). (Contributed by Alexander van der Vekens, 26-May-2017.)
⊢ dom 𝐹 = (𝑆 × 𝑆)    &   ⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → ((𝐴𝐹𝐵)) ∈ 𝑆)    &   ⊢ ((𝐴𝐹𝐵)) ∈ V    ⇒   ⊢ ((𝐴𝐹𝐵)) ∈ 𝑆
Theorem	ndmaovrcl 47796	Reverse closure law, in contrast to ndmovrcl 7586 where it is required that the operation's domain doesn't contain the empty set (¬ ∅ ∈ 𝑆), no additional asumption is required. (Contributed by Alexander van der Vekens, 26-May-2017.)
⊢ dom 𝐹 = (𝑆 × 𝑆)    ⇒   ⊢ ( ((𝐴𝐹𝐵)) ∈ 𝑆 → (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆))
Theorem	ndmaovcom 47797	Any operation is commutative outside its domain, analogous to ndmovcom 7587. (Contributed by Alexander van der Vekens, 26-May-2017.)
⊢ dom 𝐹 = (𝑆 × 𝑆)    ⇒   ⊢ (¬ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → ((𝐴𝐹𝐵)) = ((𝐵𝐹𝐴)) )
Theorem	ndmaovass 47798	Any operation is associative outside its domain. In contrast to ndmovass 7588 where it is required that the operation's domain doesn't contain the empty set (¬ ∅ ∈ 𝑆), no additional assumption is required. (Contributed by Alexander van der Vekens, 26-May-2017.)
⊢ dom 𝐹 = (𝑆 × 𝑆)    ⇒   ⊢ (¬ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) → (( ((𝐴𝐹𝐵)) 𝐹𝐶)) = ((𝐴𝐹 ((𝐵𝐹𝐶)) )) )
Theorem	ndmaovdistr 47799	Any operation is distributive outside its domain. In contrast to ndmovdistr 7589 where it is required that the operation's domain doesn't contain the empty set (¬ ∅ ∈ 𝑆), no additional assumption is required. (Contributed by Alexander van der Vekens, 26-May-2017.)
⊢ dom 𝐹 = (𝑆 × 𝑆)    &   ⊢ dom 𝐺 = (𝑆 × 𝑆)    ⇒   ⊢ (¬ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) → ((𝐴𝐺 ((𝐵𝐹𝐶)) )) = (( ((𝐴𝐺𝐵)) 𝐹 ((𝐴𝐺𝐶)) )) )
21.48.5  Alternative definitions of function values (2) In the following, a second approach is followed to define function values alternately to df-afv 47712. The current definition of the value (𝐹‘𝐴) of a function 𝐹 at an argument 𝐴 (see df-fv 6533) assures that this value is always a set, see fex 7214. 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 6903 and fvprc 6863). "(𝐹‘𝐴) is meaningful" means "the class 𝐹 regarded as function is defined at the argument 𝐴" in this context. This is also expressed by 𝐹 defAt 𝐴, see df-dfat 47711. In the theory of partial functions, it is a common case that 𝐹 is not defined at 𝐴. 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 ∅ ∉ ran 𝐹, ∅ ∈ ran 𝐹, 𝐹 defAt 𝐴, or Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹 (see, for example, ndmfvrcl 6904). To avoid such an ambiguity, an alternative definition (𝐹''''𝐴) (see df-afv2 47801) would be possible which evaluates to a set not belonging to the range of 𝐹 ((𝐹''''𝐴) = 𝒫 ∪ ran 𝐹) if it is not meaningful (see ndfatafv2 47803). We say "(𝐹''''𝐴) is not defined (or undefined)" if (𝐹''''𝐴) is not in the range of 𝐹 ((𝐹''''𝐴) ∉ ran 𝐹). Because of afv2ndefb 47816, this is equivalent to ((𝐹''''𝐴) = 𝒫 ∪ ran 𝐹. If (𝐹''''𝐴) is in the range of 𝐹 ((𝐹''''𝐴) ∈ ran 𝐹), we say that "(𝐹''''𝐴) is defined". If ran 𝐹 is a set, we can use the symbol Undef to express that (𝐹''''𝐴) is not defined: (𝐹''''𝐴) = (Undef‘ran 𝐹) (see ndfatafv2undef 47804). We could have used this symbol directly to define the alternate value of a function, which would have the advantage that (𝐹''''𝐴) would always be a set. But first this symbol is defined using the original function value, which would not make it possible to replace the original definition by the alternate definition, and second we would have to assume that ran 𝐹 ∈ V in most of the theorems. To summarize, that means (𝐹''''𝐴) ∉ ran 𝐹 → (𝐹‘𝐴) = ∅ (see afv2ndeffv0 47852), but (𝐹‘𝐴) = ∅ → (𝐹''''𝐴) ∉ ran 𝐹 is not generally valid, see afv2fv0 47857. The alternate definition, however, corresponds to the current definition ((𝐹‘𝐴) = (𝐹''''𝐴)) if the function 𝐹 is defined at 𝐴 (see dfatafv2eqfv 47853). With this definition the following intuitive equivalence holds: (𝐹 defAt 𝐴 ↔ (𝐹''''𝐴) ∈ ran 𝐹), see dfatafv2rnb 47819. 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 24) proofs using the definition df-fv 6533 of (𝐹‘𝐴), we see that analogues for the following 7 theorems can be proven using the alternative definition: fveq1 6870-> afv2eq1 47808, fveq2 6871-> afv2eq2 47809, nffv 6881-> nfafv2 47810, csbfv12 6916-> csbafv212g , rlimdm 15592-> rlimdmafv2 47850, tz6.12-1 6894-> tz6.12-1-afv2 47833, fveu 6860-> afv2eu 47830. Six theorems proved by directly using df-fv 6533 are within a mathbox (fvsb 45025, uncov 38112) or not used (rlimdmafv 47769, avril1 30723) or experimental (dfafv2 47724, dfafv22 47851). However, the remaining 11 theorems proved by directly using df-fv 6533 are used more or less often: * fvex 6884: used in about 1600 proofs: Only if the function is defined at the argument, or the range of the function/class is a set, analog theorems can be proven (dfatafv2ex 47805 resp. afv2ex 47806). All of these 1600 proofs have to be checked if one of these two theorems can be used instead of fvex 6884. * fvres 6890: used in about 400 proofs : Only if the function is defined at the argument, an analog theorem can be proven (afv2res 47831). In the undefined case such a theorem cannot exist (without additional assumptions), because the range of (𝐹 ↾ 𝐵) is mostly different from the range of 𝐹, and therefore also the "undefined" values are different. All of these 400 proofs have to be checked if afv2res 47831 can be used instead of fvres 6890. * tz6.12-2 6858 (-> tz6.12-2-afv2 47829): root theorem of many theorems which have not a strict analogue, and which are used many times: ** fvprc 6863 (-> afv2prc 47818), used in 193 proofs, ** tz6.12i 6897 (-> tz6.12i-afv2 47835), used - indirectly via fvbr0 6898 and fvrn0 6899 - in 19 proofs, and in fvclss 7229 used in fvclex 7944 used in fvresex 7945 (which is not used!) and in dcomex 10419 (used in 4 proofs), ** ndmfv 6903 (-> ndmafv2nrn ), used in 124 proofs ** nfunsn 6910 (-> nfunsnafv2 ), used by fvfundmfvn0 6911 (used in 3 proofs), and dffv2 6966 (not used) ** funpartfv 36308, setrec2lem1 50322 (mathboxes) * fv2 6866: only used by elfv 6869, which is only used by fv3 6889, which is not used. * dffv3 6867 (-> dfafv23 ): used by dffv4 6868 (the previous "df-fv"), which now is only used in mathboxes (csbfv12gALTVD 45472), by shftval 15101 (itself used in 11 proofs), by dffv5 36285 (mathbox) and by fvco2 6968 (-> afv2co2 47849). * fvopab5 7013: used only by ajval 31122 (not used) and by adjval 32151, which is used in adjval2 32152 (not used) and in adjbdln 32344 (used in 7 proofs). * zsum 15759: used (via isum 15760, sum0 15762, sumss 15765 and fsumsers 15769) in 76 proofs. * isumshft 15883: used in pserdv2 26551 (used in logtayl 26783, binomcxplemdvsum 44929) , eftlub 16155 (used in 4 proofs), binomcxplemnotnn0 44930 (used in binomcxp 44931 only) and logtayl 26783 (used in 4 proofs). * ovtpos 8225: used in 16 proofs. * zprod 15981: used in 3 proofs: iprod 15982, zprodn0 15983 and prodss 15991 * iprodclim3 16044: not used! 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 6866, dffv3 6867, fvopab5 7013, zsum 15759, isumshft 15883, ovtpos 8225 and zprod 15981 are not critical or are, hopefully, also valid for the alternative definition, fvex 6884, fvres 6890 and tz6.12-2 6858 (and the theorems based on them) are essential for the current definition of function values.
Syntax	cafv2 47800	Extend the definition of a class to include the alternate function value. Read: "the value of 𝐹 at 𝐴 " or "𝐹 of 𝐴". For using several apostrophes as a symbol see comment for cafv 47709.
class (𝐹''''𝐴)