HomeTheorem List (p. 412 of 426)
Unicode version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 412 of 426) | < Previous Next > |
| Browser slow? Try the
Unicode version. |
||
|
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
||
| Color key: | Metamath Proof Explorer
(1-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | twonotinotbothi 41101 | From these two negated implications it is not the case their non negated forms are both true. (Contributed by Jarvin Udandy, 11-Sep-2020.) |
    
   
  ![/\](wedge.gif "/\"){kind=small} | ||
| Theorem | clifte 41102 | show d is the same as an if-else involving a,b. (Contributed by Jarvin Udandy, 20-Sep-2020.) |
  | ||
| Theorem | cliftet 41103 | show d is the same as an if-else involving a,b. (Contributed by Jarvin Udandy, 20-Sep-2020.) |
| | ||
| Theorem | clifteta 41104 | show d is the same as an if-else involving a,b. (Contributed by Jarvin Udandy, 20-Sep-2020.) |
|
| ||
| Theorem | cliftetb 41105 | show d is the same as an if-else involving a,b. (Contributed by Jarvin Udandy, 20-Sep-2020.) |
|
| ||
| Theorem | confun 41106 | Given the hypotheses there exists a proof for (c implies ( d iff a ) ). (Contributed by Jarvin Udandy, 6-Sep-2020.) |
| | ||
| Theorem | confun2 41107 | Confun simplified to two propositions. (Contributed by Jarvin Udandy, 6-Sep-2020.) |
|
| ||
| Theorem | confun3 41108 | Confun's more complex form where both a,d have been "defined". (Contributed by Jarvin Udandy, 6-Sep-2020.) |
|
| ||
| Theorem | confun4 41109 | An attempt at derivative. Resisted simplest path to a proof. (Contributed by Jarvin Udandy, 6-Sep-2020.) |
  | ||
| Theorem | confun5 41110 | An attempt at derivative. Resisted simplest path to a proof. Interesting that ch, th, ta, et were all provable. (Contributed by Jarvin Udandy, 7-Sep-2020.) |
|
| ||
| Theorem | plcofph 41111 | Given, a,b and a "definition" for c, c is demonstrated. (Contributed by Jarvin Udandy, 8-Sep-2020.) |
|
| ||
| Theorem | pldofph 41112 | Given, a,b c, d, "definition" for e, e is demonstrated. (Contributed by Jarvin Udandy, 8-Sep-2020.) |
| | ||
| Theorem | plvcofph 41113 | Given, a,b,d, and "definitions" for c, e, f: f is demonstrated. (Contributed by Jarvin Udandy, 8-Sep-2020.) |
|
| ||
| Theorem | plvcofphax 41114 | Given, a,b,d, and "definitions" for c, e, f, g: g is demonstrated. (Contributed by Jarvin Udandy, 8-Sep-2020.) |
 | ||
| Theorem | plvofpos 41115 | rh is derivable because ONLY one of ch, th, ta, et is implied by mu. (Contributed by Jarvin Udandy, 11-Sep-2020.) |
  | ||
| Theorem | mdandyv0 41116 | Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ph, ps accordingly. (Contributed by Jarvin Udandy, 6-Sep-2016.) |
 
| ||
| Theorem | mdandyv1 41117 | Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ph, ps accordingly. (Contributed by Jarvin Udandy, 6-Sep-2016.) |
|
| ||
| Theorem | mdandyv2 41118 | Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ph, ps accordingly. (Contributed by Jarvin Udandy, 6-Sep-2016.) |
|
| ||
| Theorem | mdandyv3 41119 | Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ph, ps accordingly. (Contributed by Jarvin Udandy, 6-Sep-2016.) |
|
| ||
| Theorem | mdandyv4 41120 | Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ph, ps accordingly. (Contributed by Jarvin Udandy, 6-Sep-2016.) |
|
| ||
| Theorem | mdandyv5 41121 | Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ph, ps accordingly. (Contributed by Jarvin Udandy, 6-Sep-2016.) |
|
| ||
| Theorem | mdandyv6 41122 | Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ph, ps accordingly. (Contributed by Jarvin Udandy, 6-Sep-2016.) |
|
| ||
| Theorem | mdandyv7 41123 | Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ph, ps accordingly. (Contributed by Jarvin Udandy, 6-Sep-2016.) |
|
| ||
| Theorem | mdandyv8 41124 | Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ph, ps accordingly. (Contributed by Jarvin Udandy, 6-Sep-2016.) |
|
| ||
| Theorem | mdandyv9 41125 | Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ph, ps accordingly. (Contributed by Jarvin Udandy, 6-Sep-2016.) |
|
| ||
| Theorem | mdandyv10 41126 | Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ph, ps accordingly. (Contributed by Jarvin Udandy, 6-Sep-2016.) |
|
| ||
| Theorem | mdandyv11 41127 | Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ph, ps accordingly. (Contributed by Jarvin Udandy, 6-Sep-2016.) |
|
| ||
| Theorem | mdandyv12 41128 | Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ph, ps accordingly. (Contributed by Jarvin Udandy, 6-Sep-2016.) |
|
| ||
| Theorem | mdandyv13 41129 | Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ph, ps accordingly. (Contributed by Jarvin Udandy, 6-Sep-2016.) |
|
| ||
| Theorem | mdandyv14 41130 | Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ph, ps accordingly. (Contributed by Jarvin Udandy, 6-Sep-2016.) |
|
| ||
| Theorem | mdandyv15 41131 | Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ph, ps accordingly. (Contributed by Jarvin Udandy, 6-Sep-2016.) |
|
| ||
| Theorem | mdandyvr0 41132 | Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ze, si accordingly. (Contributed by Jarvin Udandy, 7-Sep-2016.) |
|
| ||
| Theorem | mdandyvr1 41133 | Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ze, si accordingly. (Contributed by Jarvin Udandy, 7-Sep-2016.) |
|
| ||
| Theorem | mdandyvr2 41134 | Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ze, si accordingly. (Contributed by Jarvin Udandy, 7-Sep-2016.) |
|
| ||
| Theorem | mdandyvr3 41135 | Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ze, si accordingly. (Contributed by Jarvin Udandy, 7-Sep-2016.) |
|
| ||
| Theorem | mdandyvr4 41136 | Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ze, si accordingly. (Contributed by Jarvin Udandy, 7-Sep-2016.) |
|
| ||
| Theorem | mdandyvr5 41137 | Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ze, si accordingly. (Contributed by Jarvin Udandy, 7-Sep-2016.) |
|
| ||
| Theorem | mdandyvr6 41138 | Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ze, si accordingly. (Contributed by Jarvin Udandy, 7-Sep-2016.) |
|
| ||
| Theorem | mdandyvr7 41139 | Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ze, si accordingly. (Contributed by Jarvin Udandy, 7-Sep-2016.) |
|
| ||
| Theorem | mdandyvr8 41140 | Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ze, si accordingly. (Contributed by Jarvin Udandy, 7-Sep-2016.) |
|
| ||
| Theorem | mdandyvr9 41141 | Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ze, si accordingly. (Contributed by Jarvin Udandy, 7-Sep-2016.) |
|
| ||
| Theorem | mdandyvr10 41142 | Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ze, si accordingly. (Contributed by Jarvin Udandy, 7-Sep-2016.) |
|
| ||
| Theorem | mdandyvr11 41143 | Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ze, si accordingly. (Contributed by Jarvin Udandy, 7-Sep-2016.) |
|
| ||
| Theorem | mdandyvr12 41144 | Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ze, si accordingly. (Contributed by Jarvin Udandy, 7-Sep-2016.) |
|
| ||
| Theorem | mdandyvr13 41145 | Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ze, si accordingly. (Contributed by Jarvin Udandy, 7-Sep-2016.) |
|
| ||
| Theorem | mdandyvr14 41146 | Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ze, si accordingly. (Contributed by Jarvin Udandy, 7-Sep-2016.) |
|
| ||
| Theorem | mdandyvr15 41147 | Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ze, si accordingly. (Contributed by Jarvin Udandy, 7-Sep-2016.) |
|
| ||
| Theorem | mdandyvrx0 41148 | Given the exclusivities set in the hypotheses, there exist a proof where ch, th, ta, et exclude ze, si accordingly. (Contributed by Jarvin Udandy, 7-Sep-2016.) |
| ||
| Theorem | mdandyvrx1 41149 | Given the exclusivities set in the hypotheses, there exist a proof where ch, th, ta, et exclude ze, si accordingly. (Contributed by Jarvin Udandy, 7-Sep-2016.) |
|
| ||
| Theorem | mdandyvrx2 41150 | Given the exclusivities set in the hypotheses, there exist a proof where ch, th, ta, et exclude ze, si accordingly. (Contributed by Jarvin Udandy, 7-Sep-2016.) |
|
| ||
| Theorem | mdandyvrx3 41151 | Given the exclusivities set in the hypotheses, there exist a proof where ch, th, ta, et exclude ze, si accordingly. (Contributed by Jarvin Udandy, 7-Sep-2016.) |
|
| ||
| Theorem | mdandyvrx4 41152 | Given the exclusivities set in the hypotheses, there exist a proof where ch, th, ta, et exclude ze, si accordingly. (Contributed by Jarvin Udandy, 7-Sep-2016.) |
|
| ||
| Theorem | mdandyvrx5 41153 | Given the exclusivities set in the hypotheses, there exist a proof where ch, th, ta, et exclude ze, si accordingly. (Contributed by Jarvin Udandy, 7-Sep-2016.) |
|
| ||
| Theorem | mdandyvrx6 41154 | Given the exclusivities set in the hypotheses, there exist a proof where ch, th, ta, et exclude ze, si accordingly. (Contributed by Jarvin Udandy, 7-Sep-2016.) |
|
| ||
| Theorem | mdandyvrx7 41155 | Given the exclusivities set in the hypotheses, there exist a proof where ch, th, ta, et exclude ze, si accordingly. (Contributed by Jarvin Udandy, 7-Sep-2016.) |
|
| ||
| Theorem | mdandyvrx8 41156 | Given the exclusivities set in the hypotheses, there exist a proof where ch, th, ta, et exclude ze, si accordingly. (Contributed by Jarvin Udandy, 7-Sep-2016.) |
|
| ||
| Theorem | mdandyvrx9 41157 | Given the exclusivities set in the hypotheses, there exist a proof where ch, th, ta, et exclude ze, si accordingly. (Contributed by Jarvin Udandy, 7-Sep-2016.) |
|
| ||
| Theorem | mdandyvrx10 41158 | Given the exclusivities set in the hypotheses, there exist a proof where ch, th, ta, et exclude ze, si accordingly. (Contributed by Jarvin Udandy, 7-Sep-2016.) |
|
| ||
| Theorem | mdandyvrx11 41159 | Given the exclusivities set in the hypotheses, there exist a proof where ch, th, ta, et exclude ze, si accordingly. (Contributed by Jarvin Udandy, 7-Sep-2016.) |
|
| ||
| Theorem | mdandyvrx12 41160 | Given the exclusivities set in the hypotheses, there exist a proof where ch, th, ta, et exclude ze, si accordingly. (Contributed by Jarvin Udandy, 7-Sep-2016.) |
|
| ||
| Theorem | mdandyvrx13 41161 | Given the exclusivities set in the hypotheses, there exist a proof where ch, th, ta, et exclude ze, si accordingly. (Contributed by Jarvin Udandy, 7-Sep-2016.) |
|
| ||
| Theorem | mdandyvrx14 41162 | Given the exclusivities set in the hypotheses, there exist a proof where ch, th, ta, et exclude ze, si accordingly. (Contributed by Jarvin Udandy, 7-Sep-2016.) |
|
| ||
| Theorem | mdandyvrx15 41163 | Given the exclusivities set in the hypotheses, there exist a proof where ch, th, ta, et exclude ze, si accordingly. (Contributed by Jarvin Udandy, 7-Sep-2016.) |
|
| ||
| Theorem | H15NH16TH15IH16 41164 | Given 15 hypotheses and a 16th hypothesis, there exists a proof the 15 imply the 16th. (Contributed by Jarvin Udandy, 8-Sep-2016.) |
  jph jps jch jth
jph jps
jch jth | ||
| Theorem | dandysum2p2e4 41165 |
CONTRADICTION PROVED AT 1 + 1 = 2 . Given the right hypotheses we can prove a dandysum of 2+2=4. The qed step is the value '4' in Decimal BEING IMPLIED by the hypotheses. Note: Values that when added which exceed a 4bit value are not supported. Note: Digits begin from left (least) to right (greatest). e.g. 1000 would be '1', 0100 would be '2'. 0010 would be '4'. How to perceive the hypotheses' bits in order: ( th <-> F. ), ( ta <-> F. ) Would be input value X's first bit, and input value Y's first bit. ( et <-> F ), ( ze <-> F. ) would be input value X's second bit, and input value Y's second bit. (Contributed by Jarvin Udandy, 6-Sep-2016.) |
|
jph jps jch
jph jps
jch
jph
jps
jch
| ||
| Theorem | mdandysum2p2e4 41166 |
CONTRADICTION PROVED AT 1 + 1 = 2 . Luckily Mario Carneiro did a
successful version of his own.
See Mario's Relevant Work: 1.3.14 Half adder and full adder in propositional calculus. Given the right hypotheses we can prove a dandysum of 2+2=4. The qed step is the value '4' in Decimal BEING IMPLIED by the hypotheses. Note: Values that when added which exceed a 4bit value are not supported. Note: Digits begin from left (least) to right (greatest). e.g. 1000 would be '1', 0100 would be '2'. 0010 would be '4'. How to perceive the hypotheses' bits in order: ( th <-> F. ), ( ta <-> F. ) Would be input value X's first bit, and input value Y's first bit. ( et <-> F. ), ( ze <-> F. ) would be input value X's second bit, and input value Y's second bit. In mdandysum2p2e4, one might imagine what jth or jta could be then do the math with their truths. Also limited to the restriction jth, jta are having opposite truths equivalent to the stated truth constants. (Contributed by Jarvin Udandy, 6-Sep-2016.) |
| jth jta jth jth jta jta jth jth jth jth jph jps jch
jph jps
jch
jph
jps
jch
| ||
| Theorem | r19.32 41167 | Theorem 19.32 of [Margaris] p. 90 with restricted quantifiers, analogous to r19.32v 3083. (Contributed by Alexander van der Vekens, 29-Jun-2017.) |
     | ||
| Theorem | rexsb 41168* | An equivalent expression for restricted existence, analogous to exsb 2468. (Contributed by Alexander van der Vekens, 1-Jul-2017.) |
 
| ||
| Theorem | rexrsb 41169* | An equivalent expression for restricted existence, analogous to exsb 2468. (Contributed by Alexander van der Vekens, 1-Jul-2017.) |
|
| ||
| Theorem | 2rexsb 41170* | An equivalent expression for double restricted existence, analogous to rexsb 41168. (Contributed by Alexander van der Vekens, 1-Jul-2017.) |
  
| ||
| Theorem | 2rexrsb 41171* | An equivalent expression for double restricted existence, analogous to 2exsb 2469. (Contributed by Alexander van der Vekens, 1-Jul-2017.) |
|
| ||
| Theorem | cbvral2 41172* | Change bound variables of double restricted universal quantification, using implicit substitution, analogous to cbvral2v 3179. (Contributed by Alexander van der Vekens, 2-Jul-2017.) |
|
| ||
| Theorem | cbvrex2 41173* | Change bound variables of double restricted universal quantification, using implicit substitution, analogous to cbvrex2v 3180. (Contributed by Alexander van der Vekens, 2-Jul-2017.) |
|
| ||
| Theorem | 2ralbiim 41174 | Split a biconditional and distribute 2 quantifiers, analogous to 2albiim 1817 and ralbiim 3069. (Contributed by Alexander van der Vekens, 2-Jul-2017.) |
|
| ||
| Theorem | raaan2 41175* | Rearrange restricted quantifiers with two different restricting classes, analogous to raaan 4082. It is necessary that either both restricting classes are empty or both are not empty. (Contributed by Alexander van der Vekens, 29-Jun-2017.) |
| ||
| Theorem | rmoimi 41176 | Restricted "at most one" is preserved through implication (note wff reversal). (Contributed by Alexander van der Vekens, 17-Jun-2017.) |
 | ||
| Theorem | 2reu5a 41177 | Double restricted existential uniqueness in terms of restricted existence and restricted "at most one." (Contributed by Alexander van der Vekens, 17-Jun-2017.) |
| ||
| Theorem | reuimrmo 41178 | Restricted uniqueness implies restricted "at most one" through implication, analogous to euimmo 2522. (Contributed by Alexander van der Vekens, 25-Jun-2017.) |
|
| ||
| Theorem | rmoanim 41179* | Introduction of a conjunct into restricted "at most one" quantifier, analogous to moanim 2529. (Contributed by Alexander van der Vekens, 25-Jun-2017.) |
| | ||
| Theorem | reuan 41180* | Introduction of a conjunct into restricted uniqueness quantifier, analogous to euan 2530. (Contributed by Alexander van der Vekens, 2-Jul-2017.) |
|
| ||
| Theorem | 2reurex 41181* | Double restricted quantification with existential uniqueness, analogous to 2euex 2544. (Contributed by Alexander van der Vekens, 24-Jun-2017.) |
|
| ||
| Theorem | 2reurmo 41182* | Double restricted quantification with restricted existential uniqueness and restricted "at most one.", analogous to 2eumo 2545. (Contributed by Alexander van der Vekens, 24-Jun-2017.) |
|
| ||
| Theorem | 2reu2rex 41183* | Double restricted existential uniqueness, analogous to 2eu2ex 2546. (Contributed by Alexander van der Vekens, 25-Jun-2017.) |
|
| ||
| Theorem | 2rmoswap 41184* | A condition allowing swap of restricted "at most one" and restricted existential quantifiers, analogous to 2moswap 2547. (Contributed by Alexander van der Vekens, 25-Jun-2017.) |
|
| ||
| Theorem | 2rexreu 41185* | Double restricted existential uniqueness implies double restricted uniqueness quantification, analogous to 2exeu 2549. (Contributed by Alexander van der Vekens, 25-Jun-2017.) |
|
| ||
| Theorem | 2reu1 41186* | Double restricted existential uniqueness. This theorem shows a condition under which a "naive" definition matches the correct one, analogous to 2eu1 2553. (Contributed by Alexander van der Vekens, 25-Jun-2017.) |
|
| ||
| Theorem | 2reu2 41187* | Double restricted existential uniqueness, analogous to 2eu2 2554. (Contributed by Alexander van der Vekens, 29-Jun-2017.) |
|
| ||
| Theorem | 2reu3 41188* | Double restricted existential uniqueness, analogous to 2eu3 2555. (Contributed by Alexander van der Vekens, 29-Jun-2017.) |
|
| ||
| Theorem | 2reu4a 41189* |
Definition of double restricted existential uniqueness ("exactly one
and exactly one
"), analogous to 2eu4 2556
with the additional
requirement that the restricting classes are not empty (which is not
necessary as shown in 2reu4 41190). (Contributed by Alexander van der
Vekens, 1-Jul-2017.)
|
| ||
| Theorem | 2reu4 41190* |
Definition of double restricted existential uniqueness ("exactly one
and exactly one
"), analogous to 2eu4 2556.
(Contributed by
Alexander van der Vekens, 1-Jul-2017.)
|
|
| ||
| Theorem | 2reu7 41191* | Two equivalent expressions for double restricted existential uniqueness, analogous to 2eu7 2559. (Contributed by Alexander van der Vekens, 2-Jul-2017.) |
|
| ||
| Theorem | 2reu8 41192* |
Two equivalent expressions for double restricted existential uniqueness,
analogous to 2eu8 2560. Curiously, we can put on either of the
internal conjuncts but not both. We can also commute
using 2reu7 41191. (Contributed by Alexander van
der Vekens, 2-Jul-2017.)
|
|
| ||
The current definition of the value
Although it is very convenient for many theorems on functions and their
proofs, there are some cases in which from
To avoid such an ambiguity, an alternative definition
In the theory of partial functions, it is a common case that
With this definition the following intuitive equivalence holds:
An interesting question would be if Three theorems proved by directly using df-fv 5896 are within a mathbox (fvsb 38656) or not used (isumclim3 14490, avril1 27319). However, the remaining 8 theorems proved by directly using df-fv 5896 are used more or less often: * fvex 6201: used in about 1750 proofs. * tz6.12-1 6210: root theorem of many theorems which have not a strict analogue, and which are used many times: fvprc 6185 (used in about 127 proofs), tz6.12i 6214 (used - indirectly via fvbr0 6215 and fvrn0 6216- in 18 proofs, and in fvclss 6500 used in fvclex 7138 used in fvresex 7139, which is not used!), dcomex 9269 (used in 4 proofs), ndmfv 6218 (used in 86 proofs) and nfunsn 6225 (used by dffv2 6271 which is not used). * fv2 6186: only used by elfv 6189, which is only used by fv3 6206, which is not used. * dffv3 6187: used by dffv4 6188 (the previous "df-fv"), which now is only used in deprecated (usage discouraged) theorems or within mathboxes (csbfv12gALTOLD 39052, csbfv12gALTVD 39135), by shftval 13814 (itself used in 9 proofs), by dffv5 32031 (mathbox) and by fvco2 6273, which has the analogue afvco2 41256. * fvopab5 6309: used only by ajval 27717 (not used) and by adjval 28749 ( used - indirectly - in 9 proofs). * zsum 14449: used (via isum 14450, sum0 14452 and fsumsers 14459) in more than 90 proofs. * isumshft 14571: used in pserdv2 24184 and (via logtayl 24406) 4 other proofs. * ovtpos 7367: 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 6186, dffv3 6187, fvopab5 6309, zsum 14449, isumshft 14571 and ovtpos 7367 are not critical or are, hopefully, also valid for the alternative definition, fvex 6201 and tz6.12-1 6210 (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
(( For additional discussions/material see https://groups.google.com/forum/#!topic/metamath/cteNUppB6A4. | ||
| Syntax | wdfat 41193 |
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/forum/#!topic/metamath/cteNUppB6A4).
|
 defAt | ||
| Syntax | cafv 41194 |
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 5896), which, by the way, was intended to
visualize that in many cases and " ' " are exchangeable, makes
reading the theorems, especially those which uses both definitions as
dfafv2 41212, very difficult, 3 apostrophes '''
are used now so that it's
easier to distinguish from df-fv 5896 and df-ima 5127. 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/forum/#!topic/metamath/cteNUppB6A4).
|
 ''' | ||
| Syntax | caov 41195 |
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 6653.
|
| (()) | ||
| Definition | df-dfat 41196 |
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 
    | ||
| Definition | df-afv 41197* |
Alternative definition of the value of a function, ''',
also known as function application. In contrast to
(see df-fv 5896 and ndmfv 6218), '''  if F is not defined for
A! (Contributed by Alexander van der Vekens, 25-May-2017.)
|
''' 
defAt   | ||
| Definition | df-aov 41198 |
Define the value of an operation. In contrast to df-ov 6653, the
alternative definition for a function value (see df-afv 41197) 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 41199* | Elemination of a restricted universal quantification under certain conditions. (Contributed by Alexander van der Vekens, 2-Aug-2017.) |
| ||
| Theorem | nvelim 41200 | If a class is the universal class it doesn't belong to any class, generalisation of nvel 4797. (Contributed by Alexander van der Vekens, 26-May-2017.) |
|
| ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |
