Home | Metamath
Proof Explorer Theorem List (p. 443 of 462) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-28971) |
Hilbert Space Explorer
(28972-30494) |
Users' Mathboxes
(30495-46134) |
Type | Label | Description |
---|---|---|
Statement | ||
Syntax | caiota 44201 | Extend class notation with an alternative for Russell's definition of a description binder (inverted iota). |
class (℩'𝑥𝜑) | ||
Theorem | aiotajust 44202* | Soundness justification theorem for df-aiota 44203. (Contributed by AV, 24-Aug-2022.) |
⊢ ∩ {𝑦 ∣ {𝑥 ∣ 𝜑} = {𝑦}} = ∩ {𝑧 ∣ {𝑥 ∣ 𝜑} = {𝑧}} | ||
Definition | df-aiota 44203* |
Alternate version of Russell's definition of a description binder, which
can be read as "the unique 𝑥 such that 𝜑", where 𝜑
ordinarily contains 𝑥 as a free variable. Our definition
is
meaningful only when there is exactly one 𝑥 such that 𝜑 is true
(see aiotaval 44213); otherwise, it is not a set (see aiotaexb 44207), or even
more concrete, it is the universe V (see aiotavb 44208). Since this
is an alternative for df-iota 6327, we call this symbol ℩'
alternate iota in the following.
The advantage of this definition is the clear distinguishability of the defined and undefined cases: the alternate iota over a wff is defined iff it is a set (see aiotaexb 44207). With the original definition, there is no corresponding theorem (∃!𝑥𝜑 ↔ (℩𝑥𝜑) ≠ ∅), because ∅ can be a valid unique set satisfying a wff (see, for example, iota0def 44158). Only the right to left implication would hold, see (negated) iotanul 6347. For defined cases, however, both definitions df-iota 6327 and df-aiota 44203 are equivalent, see reuaiotaiota 44206. (Proposed by BJ, 13-Aug-2022.) (Contributed by AV, 24-Aug-2022.) |
⊢ (℩'𝑥𝜑) = ∩ {𝑦 ∣ {𝑥 ∣ 𝜑} = {𝑦}} | ||
Theorem | dfaiota2 44204* | Alternate definition of the alternate version of Russell's definition of a description binder. Definition 8.18 in [Quine] p. 56. (Contributed by AV, 24-Aug-2022.) |
⊢ (℩'𝑥𝜑) = ∩ {𝑦 ∣ ∀𝑥(𝜑 ↔ 𝑥 = 𝑦)} | ||
Theorem | reuabaiotaiota 44205* | The iota and the alternate iota over a wff 𝜑 are equal iff there is a unique satisfying value of {𝑥 ∣ 𝜑} = {𝑦}. (Contributed by AV, 25-Aug-2022.) |
⊢ (∃!𝑦{𝑥 ∣ 𝜑} = {𝑦} ↔ (℩𝑥𝜑) = (℩'𝑥𝜑)) | ||
Theorem | reuaiotaiota 44206 | The iota and the alternate iota over a wff 𝜑 are equal iff there is a unique value 𝑥 satisfying 𝜑. (Contributed by AV, 25-Aug-2022.) |
⊢ (∃!𝑥𝜑 ↔ (℩𝑥𝜑) = (℩'𝑥𝜑)) | ||
Theorem | aiotaexb 44207 | The alternate iota over a wff 𝜑 is a set iff there is a unique value 𝑥 satisfying 𝜑. (Contributed by AV, 25-Aug-2022.) |
⊢ (∃!𝑥𝜑 ↔ (℩'𝑥𝜑) ∈ V) | ||
Theorem | aiotavb 44208 | The alternate iota over a wff 𝜑 is the universe iff there is no unique value 𝑥 satisfying 𝜑. (Contributed by AV, 25-Aug-2022.) |
⊢ (¬ ∃!𝑥𝜑 ↔ (℩'𝑥𝜑) = V) | ||
Theorem | aiotaint 44209 | This is to df-aiota 44203 what iotauni 6344 is to df-iota 6327 (it uses intersection like df-aiota 44203, similar to iotauni 6344 using union like df-iota 6327; we could also prove an analogous result using union here too, in the same way that we have iotaint 6345). (Contributed by BJ, 31-Aug-2024.) |
⊢ (∃!𝑥𝜑 → (℩'𝑥𝜑) = ∩ {𝑥 ∣ 𝜑}) | ||
Theorem | dfaiota3 44210 | Alternate definition of ℩': this is to df-aiota 44203 what dfiota4 6361 is to df-iota 6327. operation using the if operator. It is simpler than df-aiota 44203 and uses no dummy variables, so it would be the preferred definition if ℩' becomes the description binder used in set.mm. (Contributed by BJ, 31-Aug-2024.) |
⊢ (℩'𝑥𝜑) = if(∃!𝑥𝜑, ∩ {𝑥 ∣ 𝜑}, V) | ||
Theorem | iotan0aiotaex 44211 | If the iota over a wff 𝜑 is not empty, the alternate iota over 𝜑 is a set. (Contributed by AV, 25-Aug-2022.) |
⊢ ((℩𝑥𝜑) ≠ ∅ → (℩'𝑥𝜑) ∈ V) | ||
Theorem | aiotaexaiotaiota 44212 | The alternate iota over a wff 𝜑 is a set iff the iota and the alternate iota over 𝜑 are equal. (Contributed by AV, 25-Aug-2022.) |
⊢ ((℩'𝑥𝜑) ∈ V ↔ (℩𝑥𝜑) = (℩'𝑥𝜑)) | ||
Theorem | aiotaval 44213* | Theorem 8.19 in [Quine] p. 57. This theorem is the fundamental property of (alternate) iota. (Contributed by AV, 24-Aug-2022.) |
⊢ (∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → (℩'𝑥𝜑) = 𝑦) | ||
Theorem | aiota0def 44214* | Example for a defined alternate iota being the empty set, i.e., ∀𝑦𝑥 ⊆ 𝑦 is a wff satisfied by a unique value 𝑥, namely 𝑥 = ∅ (the empty set is the one and only set which is a subset of every set). This corresponds to iota0def 44158. (Contributed by AV, 25-Aug-2022.) |
⊢ (℩'𝑥∀𝑦 𝑥 ⊆ 𝑦) = ∅ | ||
Theorem | aiota0ndef 44215* | Example for an undefined alternate iota being no set, i.e., ∀𝑦𝑦 ∈ 𝑥 is a wff not satisfied by a (unique) value 𝑥 (there is no set, and therefore certainly no unique set, which contains every set). This is different from iota0ndef 44159, where the iota still is a set (the empty set). (Contributed by AV, 25-Aug-2022.) |
⊢ (℩'𝑥∀𝑦 𝑦 ∈ 𝑥) ∉ V | ||
Theorem | r19.32 44216 | Theorem 19.32 of [Margaris] p. 90 with restricted quantifiers, analogous to r19.32v 3247. (Contributed by Alexander van der Vekens, 29-Jun-2017.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∨ 𝜓) ↔ (𝜑 ∨ ∀𝑥 ∈ 𝐴 𝜓)) | ||
Theorem | rexsb 44217* | An equivalent expression for restricted existence, analogous to exsb 2357. (Contributed by Alexander van der Vekens, 1-Jul-2017.) |
⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 ∀𝑥(𝑥 = 𝑦 → 𝜑)) | ||
Theorem | rexrsb 44218* | An equivalent expression for restricted existence, analogous to exsb 2357. (Contributed by Alexander van der Vekens, 1-Jul-2017.) |
⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝑥 = 𝑦 → 𝜑)) | ||
Theorem | 2rexsb 44219* | An equivalent expression for double restricted existence, analogous to rexsb 44217. (Contributed by Alexander van der Vekens, 1-Jul-2017.) |
⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 ∀𝑥∀𝑦((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝜑)) | ||
Theorem | 2rexrsb 44220* | An equivalent expression for double restricted existence, analogous to 2exsb 2358. (Contributed by Alexander van der Vekens, 1-Jul-2017.) |
⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝜑)) | ||
Theorem | cbvral2 44221* | Change bound variables of double restricted universal quantification, using implicit substitution, analogous to cbvral2v 3367. (Contributed by Alexander van der Vekens, 2-Jul-2017.) |
⊢ Ⅎ𝑧𝜑 & ⊢ Ⅎ𝑥𝜒 & ⊢ Ⅎ𝑤𝜒 & ⊢ Ⅎ𝑦𝜓 & ⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜒)) & ⊢ (𝑦 = 𝑤 → (𝜒 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐵 𝜓) | ||
Theorem | cbvrex2 44222* | Change bound variables of double restricted universal quantification, using implicit substitution, analogous to cbvrex2v 3368. (Contributed by Alexander van der Vekens, 2-Jul-2017.) |
⊢ Ⅎ𝑧𝜑 & ⊢ Ⅎ𝑥𝜒 & ⊢ Ⅎ𝑤𝜒 & ⊢ Ⅎ𝑦𝜓 & ⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜒)) & ⊢ (𝑦 = 𝑤 → (𝜒 ↔ 𝜓)) ⇒ ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝜓) | ||
Theorem | ralndv1 44223 | 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 44224 | 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 | ||
Theorem | reuf1odnf 44225* | There is exactly one element in each of two isomorphic sets. Variant of reuf1od 44226 with no distinct variable condition for 𝜒. (Contributed by AV, 19-Mar-2023.) |
⊢ (𝜑 → 𝐹:𝐶–1-1-onto→𝐵) & ⊢ ((𝜑 ∧ 𝑥 = (𝐹‘𝑦)) → (𝜓 ↔ 𝜒)) & ⊢ (𝑥 = 𝑧 → (𝜓 ↔ 𝜃)) & ⊢ Ⅎ𝑥𝜒 ⇒ ⊢ (𝜑 → (∃!𝑥 ∈ 𝐵 𝜓 ↔ ∃!𝑦 ∈ 𝐶 𝜒)) | ||
Theorem | reuf1od 44226* | There is exactly one element in each of two isomorphic sets. (Contributed by AV, 19-Mar-2023.) |
⊢ (𝜑 → 𝐹:𝐶–1-1-onto→𝐵) & ⊢ ((𝜑 ∧ 𝑥 = (𝐹‘𝑦)) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃!𝑥 ∈ 𝐵 𝜓 ↔ ∃!𝑦 ∈ 𝐶 𝜒)) | ||
Theorem | euoreqb 44227* | 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.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (∃!𝑥 ∈ 𝑉 (𝑥 = 𝐴 ∨ 𝑥 = 𝐵) ↔ 𝐴 = 𝐵)) | ||
Theorem | 2reu3 44228* | Double restricted existential uniqueness, analogous to 2eu3 2652. (Contributed by Alexander van der Vekens, 29-Jun-2017.) |
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (∃*𝑥 ∈ 𝐴 𝜑 ∨ ∃*𝑦 ∈ 𝐵 𝜑) → ((∃!𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 𝜑 ∧ ∃!𝑦 ∈ 𝐵 ∃!𝑥 ∈ 𝐴 𝜑) ↔ (∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃!𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑))) | ||
Theorem | 2reu7 44229* | Two equivalent expressions for double restricted existential uniqueness, analogous to 2eu7 2656. (Contributed by Alexander van der Vekens, 2-Jul-2017.) |
⊢ ((∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃!𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) ↔ ∃!𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑦 ∈ 𝐵 𝜑)) | ||
Theorem | 2reu8 44230* | Two equivalent expressions for double restricted existential uniqueness, analogous to 2eu8 2657. Curiously, we can put ∃! on either of the internal conjuncts but not both. We can also commute ∃!𝑥 ∈ 𝐴∃!𝑦 ∈ 𝐵 using 2reu7 44229. (Contributed by Alexander van der Vekens, 2-Jul-2017.) |
⊢ (∃!𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑦 ∈ 𝐵 𝜑) ↔ ∃!𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 (∃!𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑦 ∈ 𝐵 𝜑)) | ||
Theorem | 2reu8i 44231* | Implication of a double restricted existential uniqueness in terms of restricted existential quantification and restricted universal quantification, see also 2reu8 44230. 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 44232* | 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 44233* | 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.) |
⊢ (𝑏 = 𝑐 → (𝜑 ↔ 𝜃)) & ⊢ (𝑎 = 𝑑 → (𝜑 ↔ 𝜒)) & ⊢ (𝑎 = 𝑑 → (𝜃 ↔ 𝜏)) & ⊢ (𝑏 = 𝑒 → (𝜑 ↔ 𝜂)) & ⊢ (𝑐 = 𝑓 → (𝜃 ↔ 𝜓)) ⇒ ⊢ ((𝑉 ≠ ∅ ∧ ∃!𝑎 ∈ 𝑉 ∃!𝑏 ∈ 𝑉 𝜑) → ∃𝑎 ∈ 𝑉 ∀𝑑 ∈ 𝑉 ∀𝑏 ∈ 𝑉 ∃𝑒 ∈ 𝑉 ∀𝑓 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ((𝜒 ∧ (𝜏 → 𝑏 = 𝑐)) → (𝜓 → (𝜂 ∧ (𝑎 = 𝑑 ∧ 𝑒 = 𝑓))))) | ||
The current definition of the value (𝐹‘𝐴) of a function 𝐹 at an argument 𝐴 (see df-fv 6377) assures that this value is always a set, see fex 7031. 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 6736 and fvprc 6698). 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 6737). To avoid such an ambiguity, an alternative definition (𝐹'''𝐴) (see df-afv 44238) would be possible which evaluates to the universal class ((𝐹'''𝐴) = V) if it is not meaningful (see afvnfundmuv 44257, ndmafv 44258, afvprc 44262 and nfunsnafv 44260), and which corresponds to the current definition ((𝐹‘𝐴) = (𝐹'''𝐴)) if it is (see afvfundmfveq 44256). That means (𝐹'''𝐴) = V → (𝐹‘𝐴) = ∅ (see afvpcfv0 44264), 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 6377 of (𝐹‘𝐴), we see that analogues for the following 8 theorems can be proven using the alternative definition: fveq1 6705-> afveq1 44252, fveq2 6706-> afveq2 44253, nffv 6716-> nfafv 44254, csbfv12 6749-> csbafv12g , fvres 6725-> afvres 44290, rlimdm 15095-> rlimdmafv 44295, tz6.12-1 6728-> tz6.12-1-afv 44292, fveu 6696-> afveu 44271. Three theorems proved by directly using df-fv 6377 are within a mathbox (fvsb 41695) or not used (isumclim3 15304, avril1 28518). However, the remaining 8 theorems proved by directly using df-fv 6377 are used more or less often: * fvex 6719: used in about 1750 proofs. * tz6.12-1 6728: root theorem of many theorems which have not a strict analogue, and which are used many times: fvprc 6698 (used in about 127 proofs), tz6.12i 6732 (used - indirectly via fvbr0 6733 and fvrn0 6734- in 18 proofs, and in fvclss 7044 used in fvclex 7721 used in fvresex 7722, which is not used!), dcomex 10044 (used in 4 proofs), ndmfv 6736 (used in 86 proofs) and nfunsn 6743 (used by dffv2 6795 which is not used). * fv2 6701: only used by elfv 6704, which is only used by fv3 6724, which is not used. * dffv3 6702: used by dffv4 6703 (the previous "df-fv"), which now is only used in deprecated (usage discouraged) theorems or within mathboxes (csbfv12gALTVD 42144), by shftval 14620 (itself used in 9 proofs), by dffv5 33920 (mathbox) and by fvco2 6797, which has the analogue afvco2 44294. * fvopab5 6839: used only by ajval 28914 (not used) and by adjval 29943 (used - indirectly - in 9 proofs). * zsum 15265: used (via isum 15266, sum0 15268 and fsumsers 15275) in more than 90 proofs. * isumshft 15384: used in pserdv2 25294 and (via logtayl 25520) 4 other proofs. * ovtpos 7972: 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 6701, dffv3 6702, fvopab5 6839, zsum 15265, isumshft 15384 and ovtpos 7972 are not critical or are, hopefully, also valid for the alternative definition, fvex 6719 and tz6.12-1 6728 (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 44239. For additional details, see https://groups.google.com/g/metamath/c/cteNUppB6A4 44239. | ||
Syntax | wdfat 44234 | 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 44235 | 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 6377), 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 44250, very difficult, 3 apostrophes ''' are used now so that it's easier to distinguish from df-fv 6377 and df-ima 5553. 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 5553). |
class (𝐹'''𝐴) | ||
Syntax | caov 44236 | 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 7205. |
class ((𝐴𝐹𝐵)) | ||
Definition | df-dfat 44237 | 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 44238* | Alternative definition of the value of a function, (𝐹'''𝐴), also known as function application. In contrast to (𝐹‘𝐴) = ∅ (see df-fv 6377 and ndmfv 6736), (𝐹'''𝐴) = 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 44239 | Define the value of an operation. In contrast to df-ov 7205, the alternative definition for a function value (see df-afv 44238) 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.) |
⊢ ((𝐴𝐹𝐵)) = (𝐹'''〈𝐴, 𝐵〉) | ||
Theorem | ralbinrald 44240* | Elemination of a restricted universal quantification under certain conditions. (Contributed by Alexander van der Vekens, 2-Aug-2017.) |
⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝑥 ∈ 𝐴 → 𝑥 = 𝑋) & ⊢ (𝑥 = 𝑋 → (𝜓 ↔ 𝜃)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ 𝜃)) | ||
Theorem | nvelim 44241 | If a class is the universal class it doesn't belong to any class, generalization of nvel 5198. (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ (𝐴 = V → ¬ 𝐴 ∈ 𝐵) | ||
Theorem | alneu 44242 | 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 44243* | 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) | ||
Theorem | dfateq12d 44244 | Equality deduction for "defined at". (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ (𝜑 → 𝐹 = 𝐺) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐹 defAt 𝐴 ↔ 𝐺 defAt 𝐵)) | ||
Theorem | nfdfat 44245 | 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 44246* | 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 44247 | A function is defined at any element of its domain. (Contributed by AV, 2-Sep-2022.) |
⊢ ((Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹) → 𝐹 defAt 𝐴) | ||
Theorem | dfatprc 44248 | A function is not defined at a proper class. (Contributed by AV, 1-Sep-2022.) |
⊢ (¬ 𝐴 ∈ V → ¬ 𝐹 defAt 𝐴) | ||
Theorem | dfatelrn 44249 | 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 𝐹) | ||
Theorem | dfafv2 44250 | 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 44251 | Equality deduction for function value, analogous to fveq12d 6713. (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ (𝜑 → 𝐹 = 𝐺) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐹'''𝐴) = (𝐺'''𝐵)) | ||
Theorem | afveq1 44252 | Equality theorem for function value, analogous to fveq1 6705. (Contributed by Alexander van der Vekens, 22-Jul-2017.) |
⊢ (𝐹 = 𝐺 → (𝐹'''𝐴) = (𝐺'''𝐴)) | ||
Theorem | afveq2 44253 | Equality theorem for function value, analogous to fveq1 6705. (Contributed by Alexander van der Vekens, 22-Jul-2017.) |
⊢ (𝐴 = 𝐵 → (𝐹'''𝐴) = (𝐹'''𝐵)) | ||
Theorem | nfafv 44254 | Bound-variable hypothesis builder for function value, analogous to nffv 6716. To prove a deduction version of this analogous to nffvd 6718 is not easily possible because a deduction version of nfdfat 44245 cannot be shown easily. (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ Ⅎ𝑥𝐹 & ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥(𝐹'''𝐴) | ||
Theorem | csbafv12g 44255 | Move class substitution in and out of a function value, analogous to csbfv12 6749, with a direct proof proposed by Mario Carneiro, analogous to csbov123 7244. (Contributed by Alexander van der Vekens, 23-Jul-2017.) |
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌(𝐹'''𝐵) = (⦋𝐴 / 𝑥⦌𝐹'''⦋𝐴 / 𝑥⦌𝐵)) | ||
Theorem | afvfundmfveq 44256 | 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 44257 | 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 44258 | The value of a class outside its domain is the universe, compare with ndmfv 6736. (Contributed by Alexander van der Vekens, 25-May-2017.) |
⊢ (¬ 𝐴 ∈ dom 𝐹 → (𝐹'''𝐴) = V) | ||
Theorem | afvvdm 44259 | 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 44260 | If the restriction of a class to a singleton is not a function, its value is the universe, compare with nfunsn 6743. (Contributed by Alexander van der Vekens, 25-May-2017.) |
⊢ (¬ Fun (𝐹 ↾ {𝐴}) → (𝐹'''𝐴) = V) | ||
Theorem | afvvfunressn 44261 | 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 44262 | A function's value at a proper class is the universe, compare with fvprc 6698. (Contributed by Alexander van der Vekens, 25-May-2017.) |
⊢ (¬ 𝐴 ∈ V → (𝐹'''𝐴) = V) | ||
Theorem | afvvv 44263 | 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 44264 | 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 44265 | 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 44266 | 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 44267 | 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 44268 | 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 44269 | 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 44270 | 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 44271* | The value of a function at a unique point, analogous to fveu 6696. (Contributed by Alexander van der Vekens, 29-Nov-2017.) |
⊢ (∃!𝑥 𝐴𝐹𝑥 → (𝐹'''𝐴) = ∪ {𝑥 ∣ 𝐴𝐹𝑥}) | ||
Theorem | fnbrafvb 44272 | Equivalence of function value and binary relation, analogous to fnbrfvb 6754. (Contributed by Alexander van der Vekens, 25-May-2017.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → ((𝐹'''𝐵) = 𝐶 ↔ 𝐵𝐹𝐶)) | ||
Theorem | fnopafvb 44273 | Equivalence of function value and ordered pair membership, analogous to fnopfvb 6755. (Contributed by Alexander van der Vekens, 25-May-2017.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → ((𝐹'''𝐵) = 𝐶 ↔ 〈𝐵, 𝐶〉 ∈ 𝐹)) | ||
Theorem | funbrafvb 44274 | Equivalence of function value and binary relation, analogous to funbrfvb 6756. (Contributed by Alexander van der Vekens, 25-May-2017.) |
⊢ ((Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹) → ((𝐹'''𝐴) = 𝐵 ↔ 𝐴𝐹𝐵)) | ||
Theorem | funopafvb 44275 | Equivalence of function value and ordered pair membership, analogous to funopfvb 6757. (Contributed by Alexander van der Vekens, 25-May-2017.) |
⊢ ((Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹) → ((𝐹'''𝐴) = 𝐵 ↔ 〈𝐴, 𝐵〉 ∈ 𝐹)) | ||
Theorem | funbrafv 44276 | The second argument of a binary relation on a function is the function's value, analogous to funbrfv 6752. (Contributed by Alexander van der Vekens, 25-May-2017.) |
⊢ (Fun 𝐹 → (𝐴𝐹𝐵 → (𝐹'''𝐴) = 𝐵)) | ||
Theorem | funbrafv2b 44277 | Function value in terms of a binary relation, analogous to funbrfv2b 6759. (Contributed by Alexander van der Vekens, 25-May-2017.) |
⊢ (Fun 𝐹 → (𝐴𝐹𝐵 ↔ (𝐴 ∈ dom 𝐹 ∧ (𝐹'''𝐴) = 𝐵))) | ||
Theorem | dfafn5a 44278* | Representation of a function in terms of its values, analogous to dffn5 6760 (only one direction of implication!). (Contributed by Alexander van der Vekens, 25-May-2017.) |
⊢ (𝐹 Fn 𝐴 → 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹'''𝑥))) | ||
Theorem | dfafn5b 44279* | Representation of a function in terms of its values, analogous to dffn5 6760 (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 44280* | The range of a function expressed as a collection of the function's values, analogous to fnrnfv 6761. (Contributed by Alexander van der Vekens, 25-May-2017.) |
⊢ (𝐹 Fn 𝐴 → ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹'''𝑥)}) | ||
Theorem | afvelrnb 44281* | A member of a function's range is a value of the function, analogous to fvelrnb 6762 with the additional requirement that the member must be a set. (Contributed by Alexander van der Vekens, 25-May-2017.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝑉) → (𝐵 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 (𝐹'''𝑥) = 𝐵)) | ||
Theorem | afvelrnb0 44282* | A member of a function's range is a value of the function, only one direction of implication of fvelrnb 6762. (Contributed by Alexander van der Vekens, 1-Jun-2017.) |
⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ ran 𝐹 → ∃𝑥 ∈ 𝐴 (𝐹'''𝑥) = 𝐵)) | ||
Theorem | dfaimafn 44283* | Alternate definition of the image of a function, analogous to dfimafn 6764. (Contributed by Alexander van der Vekens, 25-May-2017.) |
⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹) → (𝐹 “ 𝐴) = {𝑦 ∣ ∃𝑥 ∈ 𝐴 (𝐹'''𝑥) = 𝑦}) | ||
Theorem | dfaimafn2 44284* | Alternate definition of the image of a function as an indexed union of singletons of function values, analogous to dfimafn2 6765. (Contributed by Alexander van der Vekens, 25-May-2017.) |
⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹) → (𝐹 “ 𝐴) = ∪ 𝑥 ∈ 𝐴 {(𝐹'''𝑥)}) | ||
Theorem | afvelima 44285* | Function value in an image, analogous to fvelima 6767. (Contributed by Alexander van der Vekens, 25-May-2017.) |
⊢ ((Fun 𝐹 ∧ 𝐴 ∈ (𝐹 “ 𝐵)) → ∃𝑥 ∈ 𝐵 (𝐹'''𝑥) = 𝐴) | ||
Theorem | afvelrn 44286 | A function's value belongs to its range, analogous to fvelrn 6886. (Contributed by Alexander van der Vekens, 25-May-2017.) |
⊢ ((Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹) → (𝐹'''𝐴) ∈ ran 𝐹) | ||
Theorem | fnafvelrn 44287 | A function's value belongs to its range, analogous to fnfvelrn 6890. (Contributed by Alexander van der Vekens, 25-May-2017.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → (𝐹'''𝐵) ∈ ran 𝐹) | ||
Theorem | fafvelrn 44288 | A function's value belongs to its codomain, analogous to ffvelrn 6891. (Contributed by Alexander van der Vekens, 25-May-2017.) |
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → (𝐹'''𝐶) ∈ 𝐵) | ||
Theorem | ffnafv 44289* | A function maps to a class to which all values belong, analogous to ffnfv 6924. (Contributed by Alexander van der Vekens, 25-May-2017.) |
⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹'''𝑥) ∈ 𝐵)) | ||
Theorem | afvres 44290 | The value of a restricted function, analogous to fvres 6725. (Contributed by Alexander van der Vekens, 22-Jul-2017.) |
⊢ (𝐴 ∈ 𝐵 → ((𝐹 ↾ 𝐵)'''𝐴) = (𝐹'''𝐴)) | ||
Theorem | tz6.12-afv 44291* | Function value. Theorem 6.12(1) of [TakeutiZaring] p. 27, analogous to tz6.12 6729. (Contributed by Alexander van der Vekens, 29-Nov-2017.) |
⊢ ((〈𝐴, 𝑦〉 ∈ 𝐹 ∧ ∃!𝑦〈𝐴, 𝑦〉 ∈ 𝐹) → (𝐹'''𝐴) = 𝑦) | ||
Theorem | tz6.12-1-afv 44292* | Function value (Theorem 6.12(1) of [TakeutiZaring] p. 27, analogous to tz6.12-1 6728. (Contributed by Alexander van der Vekens, 29-Nov-2017.) |
⊢ ((𝐴𝐹𝑦 ∧ ∃!𝑦 𝐴𝐹𝑦) → (𝐹'''𝐴) = 𝑦) | ||
Theorem | dmfcoafv 44293 | Domains of a function composition, analogous to dmfco 6796. (Contributed by Alexander van der Vekens, 23-Jul-2017.) |
⊢ ((Fun 𝐺 ∧ 𝐴 ∈ dom 𝐺) → (𝐴 ∈ dom (𝐹 ∘ 𝐺) ↔ (𝐺'''𝐴) ∈ dom 𝐹)) | ||
Theorem | afvco2 44294 | Value of a function composition, analogous to fvco2 6797. (Contributed by Alexander van der Vekens, 23-Jul-2017.) |
⊢ ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → ((𝐹 ∘ 𝐺)'''𝑋) = (𝐹'''(𝐺'''𝑋))) | ||
Theorem | rlimdmafv 44295 | Two ways to express that a function has a limit, analogous to rlimdm 15095. (Contributed by Alexander van der Vekens, 27-Nov-2017.) |
⊢ (𝜑 → 𝐹:𝐴⟶ℂ) & ⊢ (𝜑 → sup(𝐴, ℝ*, < ) = +∞) ⇒ ⊢ (𝜑 → (𝐹 ∈ dom ⇝𝑟 ↔ 𝐹 ⇝𝑟 ( ⇝𝑟 '''𝐹))) | ||
Theorem | aoveq123d 44296 | Equality deduction for operation value, analogous to oveq123d 7223. (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ (𝜑 → 𝐹 = 𝐺) & ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → ((𝐴𝐹𝐶)) = ((𝐵𝐺𝐷)) ) | ||
Theorem | nfaov 44297 | Bound-variable hypothesis builder for operation value, analogous to nfov 7232. To prove a deduction version of this analogous to nfovd 7231 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 44254). (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐹 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥 ((𝐴𝐹𝐵)) | ||
Theorem | csbaovg 44298 | Move class substitution in and out of an operation. (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ (𝐴 ∈ 𝐷 → ⦋𝐴 / 𝑥⦌ ((𝐵𝐹𝐶)) = ((⦋𝐴 / 𝑥⦌𝐵⦋𝐴 / 𝑥⦌𝐹⦋𝐴 / 𝑥⦌𝐶)) ) | ||
Theorem | aovfundmoveq 44299 | 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 44300 | 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) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |