P. 447 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 44601-44700   *Has distinct variable group(s)

Type	Label	Description
Statement
20.41.3  Double restricted existential uniqueness
20.41.3.1  Restricted quantification (extension)
Theorem	r19.32 44601	Theorem 19.32 of [Margaris] p. 90 with restricted quantifiers, analogous to r19.32v 3271. (Contributed by Alexander van der Vekens, 29-Jun-2017.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∨ 𝜓) ↔ (𝜑 ∨ ∀𝑥 ∈ 𝐴 𝜓))
Theorem	rexsb 44602*	An equivalent expression for restricted existence, analogous to exsb 2358. (Contributed by Alexander van der Vekens, 1-Jul-2017.)
⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 ∀𝑥(𝑥 = 𝑦 → 𝜑))
Theorem	rexrsb 44603*	An equivalent expression for restricted existence, analogous to exsb 2358. (Contributed by Alexander van der Vekens, 1-Jul-2017.)
⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝑥 = 𝑦 → 𝜑))
Theorem	2rexsb 44604*	An equivalent expression for double restricted existence, analogous to rexsb 44602. (Contributed by Alexander van der Vekens, 1-Jul-2017.)
⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 ∀𝑥∀𝑦((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝜑))
Theorem	2rexrsb 44605*	An equivalent expression for double restricted existence, analogous to 2exsb 2359. (Contributed by Alexander van der Vekens, 1-Jul-2017.)
⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝜑))
Theorem	cbvral2 44606*	Change bound variables of double restricted universal quantification, using implicit substitution, analogous to cbvral2v 3400. (Contributed by Alexander van der Vekens, 2-Jul-2017.)
⊢ Ⅎ𝑧𝜑    &   ⊢ Ⅎ𝑥𝜒    &   ⊢ Ⅎ𝑤𝜒    &   ⊢ Ⅎ𝑦𝜓    &   ⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑦 = 𝑤 → (𝜒 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐵 𝜓)
Theorem	cbvrex2 44607*	Change bound variables of double restricted universal quantification, using implicit substitution, analogous to cbvrex2v 3401. (Contributed by Alexander van der Vekens, 2-Jul-2017.)
⊢ Ⅎ𝑧𝜑    &   ⊢ Ⅎ𝑥𝜒    &   ⊢ Ⅎ𝑤𝜒    &   ⊢ Ⅎ𝑦𝜓    &   ⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑦 = 𝑤 → (𝜒 ↔ 𝜓))    ⇒   ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝜓)
Theorem	ralndv1 44608	Example for a theorem about a restricted universal quantification in which the restricting class depends on (actually is) the bound variable: All sets containing themselves contain the universal class. (Contributed by AV, 24-Jun-2023.)
⊢ ∀𝑥 ∈ 𝑥 V ∈ 𝑥
Theorem	ralndv2 44609	Second example for a theorem about a restricted universal quantification in which the restricting class depends on the bound variable: all subsets of a set are sets. (Contributed by AV, 24-Jun-2023.)
⊢ ∀𝑥 ∈ 𝒫 𝑥𝑥 ∈ V
20.41.3.2  Restricted uniqueness and "at most one" quantification
Theorem	reuf1odnf 44610*	There is exactly one element in each of two isomorphic sets. Variant of reuf1od 44611 with no distinct variable condition for 𝜒. (Contributed by AV, 19-Mar-2023.)
⊢ (𝜑 → 𝐹:𝐶–1-1-onto→𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 = (𝐹‘𝑦)) → (𝜓 ↔ 𝜒))    &   ⊢ (𝑥 = 𝑧 → (𝜓 ↔ 𝜃))    &   ⊢ Ⅎ𝑥𝜒    ⇒   ⊢ (𝜑 → (∃!𝑥 ∈ 𝐵 𝜓 ↔ ∃!𝑦 ∈ 𝐶 𝜒))
Theorem	reuf1od 44611*	There is exactly one element in each of two isomorphic sets. (Contributed by AV, 19-Mar-2023.)
⊢ (𝜑 → 𝐹:𝐶–1-1-onto→𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 = (𝐹‘𝑦)) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃!𝑥 ∈ 𝐵 𝜓 ↔ ∃!𝑦 ∈ 𝐶 𝜒))
Theorem	euoreqb 44612*	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.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (∃!𝑥 ∈ 𝑉 (𝑥 = 𝐴 ∨ 𝑥 = 𝐵) ↔ 𝐴 = 𝐵))
20.41.3.3  Analogs to Existential uniqueness (double quantification)
Theorem	2reu3 44613*	Double restricted existential uniqueness, analogous to 2eu3 2656. (Contributed by Alexander van der Vekens, 29-Jun-2017.)
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (∃*𝑥 ∈ 𝐴 𝜑 ∨ ∃*𝑦 ∈ 𝐵 𝜑) → ((∃!𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 𝜑 ∧ ∃!𝑦 ∈ 𝐵 ∃!𝑥 ∈ 𝐴 𝜑) ↔ (∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃!𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑)))
Theorem	2reu7 44614*	Two equivalent expressions for double restricted existential uniqueness, analogous to 2eu7 2660. (Contributed by Alexander van der Vekens, 2-Jul-2017.)
⊢ ((∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃!𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) ↔ ∃!𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑦 ∈ 𝐵 𝜑))
Theorem	2reu8 44615*	Two equivalent expressions for double restricted existential uniqueness, analogous to 2eu8 2661. Curiously, we can put ∃! on either of the internal conjuncts but not both. We can also commute ∃!𝑥 ∈ 𝐴∃!𝑦 ∈ 𝐵 using 2reu7 44614. (Contributed by Alexander van der Vekens, 2-Jul-2017.)
⊢ (∃!𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑦 ∈ 𝐵 𝜑) ↔ ∃!𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 (∃!𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑦 ∈ 𝐵 𝜑))
20.41.3.4  Additional theorems for double restricted existential uniqueness
Theorem	2reu8i 44616*	Implication of a double restricted existential uniqueness in terms of restricted existential quantification and restricted universal quantification, see also 2reu8 44615. 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 44617*	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 44618*	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.)
⊢ (𝑏 = 𝑐 → (𝜑 ↔ 𝜃))    &   ⊢ (𝑎 = 𝑑 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑎 = 𝑑 → (𝜃 ↔ 𝜏))    &   ⊢ (𝑏 = 𝑒 → (𝜑 ↔ 𝜂))    &   ⊢ (𝑐 = 𝑓 → (𝜃 ↔ 𝜓))    ⇒   ⊢ ((𝑉 ≠ ∅ ∧ ∃!𝑎 ∈ 𝑉 ∃!𝑏 ∈ 𝑉 𝜑) → ∃𝑎 ∈ 𝑉 ∀𝑑 ∈ 𝑉 ∀𝑏 ∈ 𝑉 ∃𝑒 ∈ 𝑉 ∀𝑓 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ((𝜒 ∧ (𝜏 → 𝑏 = 𝑐)) → (𝜓 → (𝜂 ∧ (𝑎 = 𝑑 ∧ 𝑒 = 𝑓)))))
20.41.4  Alternative definitions of function and operation values The current definition of the value (𝐹‘𝐴) of a function 𝐹 at an argument 𝐴 (see df-fv 6445) assures that this value is always a set, see fex 7111. 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 6813 and fvprc 6775). 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 6814). To avoid such an ambiguity, an alternative definition (𝐹'''𝐴) (see df-afv 44623) would be possible which evaluates to the universal class ((𝐹'''𝐴) = V) if it is not meaningful (see afvnfundmuv 44642, ndmafv 44643, afvprc 44647 and nfunsnafv 44645), and which corresponds to the current definition ((𝐹‘𝐴) = (𝐹'''𝐴)) if it is (see afvfundmfveq 44641). That means (𝐹'''𝐴) = V → (𝐹‘𝐴) = ∅ (see afvpcfv0 44649), 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 6445 of (𝐹‘𝐴), we see that analogues for the following 8 theorems can be proven using the alternative definition: fveq1 6782-> afveq1 44637, fveq2 6783-> afveq2 44638, nffv 6793-> nfafv 44639, csbfv12 6826-> csbafv12g , fvres 6802-> afvres 44675, rlimdm 15269-> rlimdmafv 44680, tz6.12-1 6805-> tz6.12-1-afv 44677, fveu 6772-> afveu 44656. Three theorems proved by directly using df-fv 6445 are within a mathbox (fvsb 42077) or not used (isumclim3 15480, avril1 28836). However, the remaining 8 theorems proved by directly using df-fv 6445 are used more or less often: * fvex 6796: used in about 1750 proofs. * tz6.12-1 6805: root theorem of many theorems which have not a strict analogue, and which are used many times: fvprc 6775 (used in about 127 proofs), tz6.12i 6809 (used - indirectly via fvbr0 6810 and fvrn0 6811- in 18 proofs, and in fvclss 7124 used in fvclex 7810 used in fvresex 7811, which is not used!), dcomex 10212 (used in 4 proofs), ndmfv 6813 (used in 86 proofs) and nfunsn 6820 (used by dffv2 6872 which is not used). * fv2 6778: only used by elfv 6781, which is only used by fv3 6801, which is not used. * dffv3 6779: used by dffv4 6780 (the previous "df-fv"), which now is only used in deprecated (usage discouraged) theorems or within mathboxes (csbfv12gALTVD 42526), by shftval 14794 (itself used in 9 proofs), by dffv5 34235 (mathbox) and by fvco2 6874, which has the analogue afvco2 44679. * fvopab5 6916: used only by ajval 29232 (not used) and by adjval 30261 (used - indirectly - in 9 proofs). * zsum 15439: used (via isum 15440, sum0 15442 and fsumsers 15449) in more than 90 proofs. * isumshft 15560: used in pserdv2 25598 and (via logtayl 25824) 4 other proofs. * ovtpos 8066: 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 6778, dffv3 6779, fvopab5 6916, zsum 15439, isumshft 15560 and ovtpos 8066 are not critical or are, hopefully, also valid for the alternative definition, fvex 6796 and tz6.12-1 6805 (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 44624. For additional details, see https://groups.google.com/g/metamath/c/cteNUppB6A4 44624.
Syntax	wdfat 44619	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 44620	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 6445), 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 44635, very difficult, 3 apostrophes ''' are used now so that it's easier to distinguish from df-fv 6445 and df-ima 5603. 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 5603).
class (𝐹'''𝐴)
Syntax	caov 44621	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 7287.
class ((𝐴𝐹𝐵))
Definition	df-dfat 44622	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 44623*	Alternative definition of the value of a function, (𝐹'''𝐴), also known as function application. In contrast to (𝐹‘𝐴) = ∅ (see df-fv 6445 and ndmfv 6813), (𝐹'''𝐴) = 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 44624	Define the value of an operation. In contrast to df-ov 7287, the alternative definition for a function value (see df-afv 44623) 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.)
⊢ ((𝐴𝐹𝐵)) = (𝐹'''⟨𝐴, 𝐵⟩)
20.41.4.1  Restricted quantification (extension)
Theorem	ralbinrald 44625*	Elemination of a restricted universal quantification under certain conditions. (Contributed by Alexander van der Vekens, 2-Aug-2017.)
⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝑥 ∈ 𝐴 → 𝑥 = 𝑋)    &   ⊢ (𝑥 = 𝑋 → (𝜓 ↔ 𝜃))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ 𝜃))
20.41.4.2  The universal class (extension)
Theorem	nvelim 44626	If a class is the universal class it doesn't belong to any class, generalization of nvel 5241. (Contributed by Alexander van der Vekens, 26-May-2017.)
⊢ (𝐴 = V → ¬ 𝐴 ∈ 𝐵)
20.41.4.3  Introduce the Axiom of Power Sets (extension)
Theorem	alneu 44627	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 44628*	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)
20.41.4.4  Predicate "defined at"
Theorem	dfateq12d 44629	Equality deduction for "defined at". (Contributed by Alexander van der Vekens, 26-May-2017.)
⊢ (𝜑 → 𝐹 = 𝐺)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐹 defAt 𝐴 ↔ 𝐺 defAt 𝐵))
Theorem	nfdfat 44630	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 44631*	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 44632	A function is defined at any element of its domain. (Contributed by AV, 2-Sep-2022.)
⊢ ((Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹) → 𝐹 defAt 𝐴)
Theorem	dfatprc 44633	A function is not defined at a proper class. (Contributed by AV, 1-Sep-2022.)
⊢ (¬ 𝐴 ∈ V → ¬ 𝐹 defAt 𝐴)
Theorem	dfatelrn 44634	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 𝐹)
20.41.4.5  Alternative definition of the value of a function
Theorem	dfafv2 44635	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 44636	Equality deduction for function value, analogous to fveq12d 6790. (Contributed by Alexander van der Vekens, 26-May-2017.)
⊢ (𝜑 → 𝐹 = 𝐺)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐹'''𝐴) = (𝐺'''𝐵))
Theorem	afveq1 44637	Equality theorem for function value, analogous to fveq1 6782. (Contributed by Alexander van der Vekens, 22-Jul-2017.)
⊢ (𝐹 = 𝐺 → (𝐹'''𝐴) = (𝐺'''𝐴))
Theorem	afveq2 44638	Equality theorem for function value, analogous to fveq1 6782. (Contributed by Alexander van der Vekens, 22-Jul-2017.)
⊢ (𝐴 = 𝐵 → (𝐹'''𝐴) = (𝐹'''𝐵))
Theorem	nfafv 44639	Bound-variable hypothesis builder for function value, analogous to nffv 6793. To prove a deduction version of this analogous to nffvd 6795 is not easily possible because a deduction version of nfdfat 44630 cannot be shown easily. (Contributed by Alexander van der Vekens, 26-May-2017.)
⊢ Ⅎ𝑥𝐹    &   ⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥(𝐹'''𝐴)
Theorem	csbafv12g 44640	Move class substitution in and out of a function value, analogous to csbfv12 6826, with a direct proof proposed by Mario Carneiro, analogous to csbov123 7326. (Contributed by Alexander van der Vekens, 23-Jul-2017.)
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌(𝐹'''𝐵) = (⦋𝐴 / 𝑥⦌𝐹'''⦋𝐴 / 𝑥⦌𝐵))
Theorem	afvfundmfveq 44641	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 44642	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 44643	The value of a class outside its domain is the universe, compare with ndmfv 6813. (Contributed by Alexander van der Vekens, 25-May-2017.)
⊢ (¬ 𝐴 ∈ dom 𝐹 → (𝐹'''𝐴) = V)
Theorem	afvvdm 44644	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 44645	If the restriction of a class to a singleton is not a function, its value is the universe, compare with nfunsn 6820. (Contributed by Alexander van der Vekens, 25-May-2017.)
⊢ (¬ Fun (𝐹 ↾ {𝐴}) → (𝐹'''𝐴) = V)
Theorem	afvvfunressn 44646	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 44647	A function's value at a proper class is the universe, compare with fvprc 6775. (Contributed by Alexander van der Vekens, 25-May-2017.)
⊢ (¬ 𝐴 ∈ V → (𝐹'''𝐴) = V)
Theorem	afvvv 44648	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 44649	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 44650	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 44651	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 44652	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 44653	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 44654	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 44655	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 44656*	The value of a function at a unique point, analogous to fveu 6772. (Contributed by Alexander van der Vekens, 29-Nov-2017.)
⊢ (∃!𝑥 𝐴𝐹𝑥 → (𝐹'''𝐴) = ∪ {𝑥 ∣ 𝐴𝐹𝑥})
Theorem	fnbrafvb 44657	Equivalence of function value and binary relation, analogous to fnbrfvb 6831. (Contributed by Alexander van der Vekens, 25-May-2017.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → ((𝐹'''𝐵) = 𝐶 ↔ 𝐵𝐹𝐶))
Theorem	fnopafvb 44658	Equivalence of function value and ordered pair membership, analogous to fnopfvb 6832. (Contributed by Alexander van der Vekens, 25-May-2017.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → ((𝐹'''𝐵) = 𝐶 ↔ ⟨𝐵, 𝐶⟩ ∈ 𝐹))
Theorem	funbrafvb 44659	Equivalence of function value and binary relation, analogous to funbrfvb 6833. (Contributed by Alexander van der Vekens, 25-May-2017.)
⊢ ((Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹) → ((𝐹'''𝐴) = 𝐵 ↔ 𝐴𝐹𝐵))
Theorem	funopafvb 44660	Equivalence of function value and ordered pair membership, analogous to funopfvb 6834. (Contributed by Alexander van der Vekens, 25-May-2017.)
⊢ ((Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹) → ((𝐹'''𝐴) = 𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝐹))
Theorem	funbrafv 44661	The second argument of a binary relation on a function is the function's value, analogous to funbrfv 6829. (Contributed by Alexander van der Vekens, 25-May-2017.)
⊢ (Fun 𝐹 → (𝐴𝐹𝐵 → (𝐹'''𝐴) = 𝐵))
Theorem	funbrafv2b 44662	Function value in terms of a binary relation, analogous to funbrfv2b 6836. (Contributed by Alexander van der Vekens, 25-May-2017.)
⊢ (Fun 𝐹 → (𝐴𝐹𝐵 ↔ (𝐴 ∈ dom 𝐹 ∧ (𝐹'''𝐴) = 𝐵)))
Theorem	dfafn5a 44663*	Representation of a function in terms of its values, analogous to dffn5 6837 (only one direction of implication!). (Contributed by Alexander van der Vekens, 25-May-2017.)
⊢ (𝐹 Fn 𝐴 → 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹'''𝑥)))
Theorem	dfafn5b 44664*	Representation of a function in terms of its values, analogous to dffn5 6837 (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 44665*	The range of a function expressed as a collection of the function's values, analogous to fnrnfv 6838. (Contributed by Alexander van der Vekens, 25-May-2017.)
⊢ (𝐹 Fn 𝐴 → ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹'''𝑥)})
Theorem	afvelrnb 44666*	A member of a function's range is a value of the function, analogous to fvelrnb 6839 with the additional requirement that the member must be a set. (Contributed by Alexander van der Vekens, 25-May-2017.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝑉) → (𝐵 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 (𝐹'''𝑥) = 𝐵))
Theorem	afvelrnb0 44667*	A member of a function's range is a value of the function, only one direction of implication of fvelrnb 6839. (Contributed by Alexander van der Vekens, 1-Jun-2017.)
⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ ran 𝐹 → ∃𝑥 ∈ 𝐴 (𝐹'''𝑥) = 𝐵))
Theorem	dfaimafn 44668*	Alternate definition of the image of a function, analogous to dfimafn 6841. (Contributed by Alexander van der Vekens, 25-May-2017.)
⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹) → (𝐹 “ 𝐴) = {𝑦 ∣ ∃𝑥 ∈ 𝐴 (𝐹'''𝑥) = 𝑦})
Theorem	dfaimafn2 44669*	Alternate definition of the image of a function as an indexed union of singletons of function values, analogous to dfimafn2 6842. (Contributed by Alexander van der Vekens, 25-May-2017.)
⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹) → (𝐹 “ 𝐴) = ∪ 𝑥 ∈ 𝐴 {(𝐹'''𝑥)})
Theorem	afvelima 44670*	Function value in an image, analogous to fvelima 6844. (Contributed by Alexander van der Vekens, 25-May-2017.)
⊢ ((Fun 𝐹 ∧ 𝐴 ∈ (𝐹 “ 𝐵)) → ∃𝑥 ∈ 𝐵 (𝐹'''𝑥) = 𝐴)
Theorem	afvelrn 44671	A function's value belongs to its range, analogous to fvelrn 6963. (Contributed by Alexander van der Vekens, 25-May-2017.)
⊢ ((Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹) → (𝐹'''𝐴) ∈ ran 𝐹)
Theorem	fnafvelrn 44672	A function's value belongs to its range, analogous to fnfvelrn 6967. (Contributed by Alexander van der Vekens, 25-May-2017.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → (𝐹'''𝐵) ∈ ran 𝐹)
Theorem	fafvelrn 44673	A function's value belongs to its codomain, analogous to ffvelrn 6968. (Contributed by Alexander van der Vekens, 25-May-2017.)
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → (𝐹'''𝐶) ∈ 𝐵)
Theorem	ffnafv 44674*	A function maps to a class to which all values belong, analogous to ffnfv 7001. (Contributed by Alexander van der Vekens, 25-May-2017.)
⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹'''𝑥) ∈ 𝐵))
Theorem	afvres 44675	The value of a restricted function, analogous to fvres 6802. (Contributed by Alexander van der Vekens, 22-Jul-2017.)
⊢ (𝐴 ∈ 𝐵 → ((𝐹 ↾ 𝐵)'''𝐴) = (𝐹'''𝐴))
Theorem	tz6.12-afv 44676*	Function value. Theorem 6.12(1) of [TakeutiZaring] p. 27, analogous to tz6.12 6806. (Contributed by Alexander van der Vekens, 29-Nov-2017.)
⊢ ((⟨𝐴, 𝑦⟩ ∈ 𝐹 ∧ ∃!𝑦⟨𝐴, 𝑦⟩ ∈ 𝐹) → (𝐹'''𝐴) = 𝑦)
Theorem	tz6.12-1-afv 44677*	Function value (Theorem 6.12(1) of [TakeutiZaring] p. 27, analogous to tz6.12-1 6805. (Contributed by Alexander van der Vekens, 29-Nov-2017.)
⊢ ((𝐴𝐹𝑦 ∧ ∃!𝑦 𝐴𝐹𝑦) → (𝐹'''𝐴) = 𝑦)
Theorem	dmfcoafv 44678	Domains of a function composition, analogous to dmfco 6873. (Contributed by Alexander van der Vekens, 23-Jul-2017.)
⊢ ((Fun 𝐺 ∧ 𝐴 ∈ dom 𝐺) → (𝐴 ∈ dom (𝐹 ∘ 𝐺) ↔ (𝐺'''𝐴) ∈ dom 𝐹))
Theorem	afvco2 44679	Value of a function composition, analogous to fvco2 6874. (Contributed by Alexander van der Vekens, 23-Jul-2017.)
⊢ ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → ((𝐹 ∘ 𝐺)'''𝑋) = (𝐹'''(𝐺'''𝑋)))
Theorem	rlimdmafv 44680	Two ways to express that a function has a limit, analogous to rlimdm 15269. (Contributed by Alexander van der Vekens, 27-Nov-2017.)
⊢ (𝜑 → 𝐹:𝐴⟶ℂ)    &   ⊢ (𝜑 → sup(𝐴, ℝ*, < ) = +∞)    ⇒   ⊢ (𝜑 → (𝐹 ∈ dom ⇝𝑟 ↔ 𝐹 ⇝𝑟 ( ⇝𝑟 '''𝐹)))
20.41.4.6  Alternative definition of the value of an operation
Theorem	aoveq123d 44681	Equality deduction for operation value, analogous to oveq123d 7305. (Contributed by Alexander van der Vekens, 26-May-2017.)
⊢ (𝜑 → 𝐹 = 𝐺)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → ((𝐴𝐹𝐶)) = ((𝐵𝐺𝐷)) )
Theorem	nfaov 44682	Bound-variable hypothesis builder for operation value, analogous to nfov 7314. To prove a deduction version of this analogous to nfovd 7313 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 44639). (Contributed by Alexander van der Vekens, 26-May-2017.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐹    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥 ((𝐴𝐹𝐵))
Theorem	csbaovg 44683	Move class substitution in and out of an operation. (Contributed by Alexander van der Vekens, 26-May-2017.)
⊢ (𝐴 ∈ 𝐷 → ⦋𝐴 / 𝑥⦌ ((𝐵𝐹𝐶)) = ((⦋𝐴 / 𝑥⦌𝐵⦋𝐴 / 𝑥⦌𝐹⦋𝐴 / 𝑥⦌𝐶)) )
Theorem	aovfundmoveq 44684	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 44685	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 44686	The value of an operation outside its domain, analogous to ndmafv 44643. (Contributed by Alexander van der Vekens, 26-May-2017.)
⊢ (¬ ⟨𝐴, 𝐵⟩ ∈ dom 𝐹 → ((𝐴𝐹𝐵)) = V)
Theorem	ndmaovg 44687	The value of an operation outside its domain, analogous to ndmovg 7464. (Contributed by Alexander van der Vekens, 26-May-2017.)
⊢ ((dom 𝐹 = (𝑅 × 𝑆) ∧ ¬ (𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆)) → ((𝐴𝐹𝐵)) = V)
Theorem	aovvdm 44688	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 44689	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 44690	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 44691	The value of an operation when the one of the arguments is a proper class, analogous to ovprc 7322. (Contributed by Alexander van der Vekens, 26-May-2017.)
⊢ Rel dom 𝐹    ⇒   ⊢ (¬ (𝐴 ∈ V ∧ 𝐵 ∈ V) → ((𝐴𝐹𝐵)) = V)
Theorem	aovrcl 44692	Reverse closure for an operation value, analogous to afvvv 44648. In contrast to ovrcl 7325, 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 44693	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 44694	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 44695	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 44696	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 44697	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 44698	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 44699	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 44700*	A frequently used special case of rspc2ev 3573 for operation values, analogous to rspceov 7331. (Contributed by Alexander van der Vekens, 26-May-2017.)
⊢ ((𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ∧ 𝑆 = ((𝐶𝐹𝐷)) ) → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑆 = ((𝑥𝐹𝑦)) )