HomeTheorem List (p. 387 of 409)
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. 387 of 409) | < 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-26619) |
Hilbert Space Explorer
(26620-28142) |
Users' Mathboxes
(28143-40812) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | mdandyvr11 38601 | 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.) |
              ![/\](wedge.gif "/\"){kind=small}
| ||
| Theorem | mdandyvr12 38602 | 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 38603 | 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 38604 | 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 38605 | 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 38606 | 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 38607 | 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 38608 | 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 38609 | 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 38610 | 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 38611 | 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 38612 | 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 38613 | 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 38614 | 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 38615 | 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 38616 | 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 38617 | 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 38618 | 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 38619 | 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 38620 | 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 38621 | 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 38622 | 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 38623 |
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 38624 |
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 38625 | Theorem 19.32 of [Margaris] p. 90 with restricted quantifiers, analogous to r19.32v 2947. (Contributed by Alexander van der Vekens, 29-Jun-2017.) |
     | ||
| Theorem | rexsb 38626* | An equivalent expression for restricted existence, analogous to exsb 2307. (Contributed by Alexander van der Vekens, 1-Jul-2017.) |
 
| ||
| Theorem | rexrsb 38627* | An equivalent expression for restricted existence, analogous to exsb 2307. (Contributed by Alexander van der Vekens, 1-Jul-2017.) |
|
| ||
| Theorem | 2rexsb 38628* | An equivalent expression for double restricted existence, analogous to rexsb 38626. (Contributed by Alexander van der Vekens, 1-Jul-2017.) |
  
| ||
| Theorem | 2rexrsb 38629* | An equivalent expression for double restricted existence, analogous to 2exsb 2308. (Contributed by Alexander van der Vekens, 1-Jul-2017.) |
|
| ||
| Theorem | cbvral2 38630* | Change bound variables of double restricted universal quantification, using implicit substitution, analogous to cbvral2v 3038. (Contributed by Alexander van der Vekens, 2-Jul-2017.) |
|
| ||
| Theorem | cbvrex2 38631* | Change bound variables of double restricted universal quantification, using implicit substitution, analogous to cbvrex2v 3039. (Contributed by Alexander van der Vekens, 2-Jul-2017.) |
|
| ||
| Theorem | 2ralbiim 38632 | Split a biconditional and distribute 2 quantifiers, analogous to 2albiim 1763 and ralbiim 2933. (Contributed by Alexander van der Vekens, 2-Jul-2017.) |
|
| ||
| Theorem | raaan2 38633* | Rearrange restricted quantifiers with two different restricting classes, analogous to raaan 3888. 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 38634 | Restricted "at most one" is preserved through implication (note wff reversal). (Contributed by Alexander van der Vekens, 17-Jun-2017.) |
 | ||
| Theorem | 2reu5a 38635 | 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 38636 | Restricted uniqueness implies restricted "at most one" through implication, analogous to euimmo 2361. (Contributed by Alexander van der Vekens, 25-Jun-2017.) |
|
| ||
| Theorem | rmoanim 38637* | Introduction of a conjunct into restricted "at most one" quantifier, analogous to moanim 2368. (Contributed by Alexander van der Vekens, 25-Jun-2017.) |
| | ||
| Theorem | reuan 38638* | Introduction of a conjunct into restricted uniqueness quantifier, analogous to euan 2369. (Contributed by Alexander van der Vekens, 2-Jul-2017.) |
|
| ||
| Theorem | 2reurex 38639* | Double restricted quantification with existential uniqueness, analogous to 2euex 2383. (Contributed by Alexander van der Vekens, 24-Jun-2017.) |
|
| ||
| Theorem | 2reurmo 38640* | Double restricted quantification with restricted existential uniqueness and restricted "at most one.", analogous to 2eumo 2384. (Contributed by Alexander van der Vekens, 24-Jun-2017.) |
|
| ||
| Theorem | 2reu2rex 38641* | Double restricted existential uniqueness, analogous to 2eu2ex 2385. (Contributed by Alexander van der Vekens, 25-Jun-2017.) |
|
| ||
| Theorem | 2rmoswap 38642* | A condition allowing swap of restricted "at most one" and restricted existential quantifiers, analogous to 2moswap 2386. (Contributed by Alexander van der Vekens, 25-Jun-2017.) |
|
| ||
| Theorem | 2rexreu 38643* | Double restricted existential uniqueness implies double restricted uniqueness quantification, analogous to 2exeu 2388. (Contributed by Alexander van der Vekens, 25-Jun-2017.) |
|
| ||
| Theorem | 2reu1 38644* | Double restricted existential uniqueness. This theorem shows a condition under which a "naive" definition matches the correct one, analogous to 2eu1 2392. (Contributed by Alexander van der Vekens, 25-Jun-2017.) |
|
| ||
| Theorem | 2reu2 38645* | Double restricted existential uniqueness, analogous to 2eu2 2393. (Contributed by Alexander van der Vekens, 29-Jun-2017.) |
|
| ||
| Theorem | 2reu3 38646* | Double restricted existential uniqueness, analogous to 2eu3 2394. (Contributed by Alexander van der Vekens, 29-Jun-2017.) |
|
| ||
| Theorem | 2reu4a 38647* |
Definition of double restricted existential uniqueness ("exactly one
and exactly one
"), analogous to 2eu4 2395
with the additional
requirement that the restricting classes are not empty (which is not
necessary as shown in 2reu4 38648). (Contributed by Alexander van der
Vekens, 1-Jul-2017.)
|
| ||
| Theorem | 2reu4 38648* |
Definition of double restricted existential uniqueness ("exactly one
and exactly one
"), analogous to 2eu4 2395.
(Contributed by
Alexander van der Vekens, 1-Jul-2017.)
|
|
| ||
| Theorem | 2reu7 38649* | Two equivalent expressions for double restricted existential uniqueness, analogous to 2eu7 2398. (Contributed by Alexander van der Vekens, 2-Jul-2017.) |
|
| ||
| Theorem | 2reu8 38650* |
Two equivalent expressions for double restricted existential uniqueness,
analogous to 2eu8 2399. Curiously, we can put on either of the
internal conjuncts but not both. We can also commute
using 2reu7 38649. (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 3 theorems proved by directly using df-fv 5608 are within a mathbox (fvsb 36848) or not used (isumclim3 13868, avril1 25948). However, the remaining 8 theorems proved by directly using df-fv 5608 are used more or less often: * fvex 5897: used in about 1750 proofs. * tz6.12-1 5903: root theorem of many theorems which have not a strict analogon, and which are used many times: fvprc 5881 (used in about 127 proofs), tz6.12i 5907 (used - indirectly via fvbr0 5908 and fvrn0 5909- in 18 proofs, and in fvclss 6171 used in fvclex 6791 used in fvresex 6792, which is not used!), dcomex 8902 (used in 4 proofs), ndmfv 5911 (used in 86 proofs) and nfunsn 5918 (used by dffv2 5960 which is not used). * fv2 5882: only used by elfv 5885, which is only used by fv3 5900, which is not used. * dffv3 5883: used by dffv4 5884 (the previous "df-fv"), which now is only used in deprecated (usage discouraged) theorems or within mathboxes (csbfv12gALTOLD 37252, csbfv12gALTVD 37335), by shftval 13185 (itself used in 9 proofs), by dffv5 30739 (mathbox) and by fvco2 5962, which has the analogon afvco2 38715. * fvopab5 5996: used only by ajval 26551 (not used) and by adjval 27591 ( used - indirectly - in 9 proofs). * zsum 13832: used (via isum 13833, sum0 13835 and fsumsers 13842) in more than 90 proofs. * isumshft 13945: used in pserdv2 23433 and (via logtayl 23653) 4 other proofs. * ovtpos 7013: used in 14 proofs. As a result of this analysis we can say that the current definition of a function's value is crucial for Metamath and cannot be exchanged easily with an alternative definition. While fv2 5882, dffv3 5883, fvopab5 5996, zsum 13832, isumshft 13945 and ovtpos 7013 are not critical or are, hopefully, also valid for the alternative definition, fvex 5897 and tz6.12-1 5903 (and the theorems based on them) are essential for the current definition of function values.
With the same arguments, an alternatvie definition of operation's values
(( For additional discussions/material see https://groups.google.com/forum/#!topic/metamath/cteNUppB6A4. | ||
| Syntax | wdfat 38651 |
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 38652 |
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 5608), 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 38671, very difficult, 3 apostrophes '''
are used now so that it's
easier to distinguish from df-fv 5608 and df-ima 4865. 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 38653 |
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 6317.
|
| (()) | ||
| Definition | df-dfat 38654 |
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 38655* |
Alternative definition of the value of a function, ''',
also known as function application. In contrast to
(see df-fv 5608 and ndmfv 5911), '''  if F is not defined for
A! (Contributed by Alexander van der Vekens, 25-May-2017.)
|
''' 
defAt   | ||
| Definition | df-aov 38656 |
Define the value of an operation. In contrast to df-ov 6317, the
alternative definition for a function value (see df-afv 38655) 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 38657* | Elemination of a restricted universal quantification under certain conditions. (Contributed by Alexander van der Vekens, 2-Aug-2017.) |
| ||
| Theorem | nvelim 38658 | If a class is the universal class it doesn't belong to any class, generalisation of nvel 4555. (Contributed by Alexander van der Vekens, 26-May-2017.) |
 | ||
| Theorem | alneu 38659 | 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 38660* | 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.) |
 | ||
| Theorem | eldmressn 38661 | Element of the domain of a restriction to a singleton. (Contributed by Alexander van der Vekens, 2-Jul-2017.) |
|
| ||
| Theorem | fveqvfvv 38662 | If a function's value at an argument is the universal class (which can never be the case because of fvex 5897), the function's value at this argument is any set (especially the empty set). In short "If a function's value is a proper class, it is a set", which sounds strange/contradictory, but which is a consequence of that a contradiction implies anything (see pm2.21i 136). (Contributed by Alexander van der Vekens, 26-May-2017.) |
|
| ||
| Theorem | funresfunco 38663 | Composition of two functions, generalization of funco 5638. (Contributed by Alexander van der Vekens, 25-Jul-2017.) |
 
 | ||
| Theorem | fnresfnco 38664 | Composition of two functions, similar to fnco 5705. (Contributed by Alexander van der Vekens, 25-Jul-2017.) |
| ||
| Theorem | funcoressn 38665 | A composition restricted to a singleton is a function under certain conditions. (Contributed by Alexander van der Vekens, 25-Jul-2017.) |
|
| ||
| Theorem | funressnfv 38666 | A restriction to a singleton with a function value is a function under certain conditions. (Contributed by Alexander van der Vekens, 25-Jul-2017.) |
|
| ||
| Theorem | fdisjdmun 38667 | The union of functions with disjoint domains is a function. (Contributed by AV, 11-Oct-2020.) |
   
  | ||
| Theorem | dfateq12d 38668 | Equality deduction for "defined at". (Contributed by Alexander van der Vekens, 26-May-2017.) |
| defAt
defAt | ||
| Theorem | nfdfat 38669 | 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, C_, etc.). (Contributed by Alexander van der Vekens, 26-May-2017.) |
 defAt | ||
| Theorem | dfdfat2 38670* |
Alternate definition of the predicate "defined at" not using the
predicate. (Contributed by Alexander van der Vekens, 22-Jul-2017.)
|
| defAt
| ||
| Theorem | dfafv2 38671 |
Alternative definition of ''' using
directly. (Contributed by Alexander van der Vekens, 22-Jul-2017.)
|
| '''
defAt | ||
| Theorem | afveq12d 38672 | Equality deduction for function value, analogous to fveq12d 5893. (Contributed by Alexander van der Vekens, 26-May-2017.) |
| ''' ''' | ||
| Theorem | afveq1 38673 | Equality theorem for function value, analogous to fveq1 5886. (Contributed by Alexander van der Vekens, 22-Jul-2017.) |
|
''' ''' | ||
| Theorem | afveq2 38674 | Equality theorem for function value, analogous to fveq1 5886. (Contributed by Alexander van der Vekens, 22-Jul-2017.) |
|
''' ''' | ||
| Theorem | nfafv 38675 | Bound-variable hypothesis builder for function value, analogous to nffv 5894. To prove a deduction version of this analogous to nffvd 5896 is not easily possible because a deduction version of nfdfat 38669 cannot be shown easily. (Contributed by Alexander van der Vekens, 26-May-2017.) |
| ''' | ||
| Theorem | csbafv12g 38676 | Move class substitution in and out of a function value, analogous to csbfv12 5922, with a direct proof proposed by Mario Carneiro, analogous to csbov123 6348. (Contributed by Alexander van der Vekens, 23-Jul-2017.) |
  ![]_](_urbrack.gif "]_"){kind=small} ''' ''' | ||
| Theorem | afvfundmfveq 38677 | 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 38678 | 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
'''
| ||
| Theorem | ndmafv 38679 | The value of a class outside its domain is the universe, compare with ndmfv 5911. (Contributed by Alexander van der Vekens, 25-May-2017.) |
| ''' | ||
| Theorem | afvvdm 38680 | 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.) |
| ''' | ||
| Theorem | nfunsnafv 38681 | If the restriction of a class to a singleton is not a function, its value is the universe, compare with nfunsn 5918. (Contributed by Alexander van der Vekens, 25-May-2017.) |
|
'''
| ||
| Theorem | afvvfunressn 38682 | 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.) |
| ''' | ||
| Theorem | afvprc 38683 | A function's value at a proper class is the universe, compare with fvprc 5881. (Contributed by Alexander van der Vekens, 25-May-2017.) |
| ''' | ||
| Theorem | afvvv 38684 | 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.) |
| ''' | ||
| Theorem | afvpcfv0 38685 | 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.) |
| '''
| ||
| Theorem | afvnufveq 38686 | 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 | afvvfveq 38687 | 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 38688 | 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 38689 | 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 38690 | 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 38691 | 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.) |
|
'''
''' | ||
| Theorem | afveu 38692* | The value of a function at a unique point, analogous to fveu 5879. (Contributed by Alexander van der Vekens, 29-Nov-2017.) |
'''   | ||
| Theorem | fnbrafvb 38693 | Equivalence of function value and binary relation, analogous to fnbrfvb 5927. (Contributed by Alexander van der Vekens, 25-May-2017.) |
| ''' | ||
| Theorem | fnopafvb 38694 | Equivalence of function value and ordered pair membership, analogous to fnopfvb 5928. (Contributed by Alexander van der Vekens, 25-May-2017.) |
| ''' | ||
| Theorem | funbrafvb 38695 | Equivalence of function value and binary relation, analogous to funbrfvb 5929. (Contributed by Alexander van der Vekens, 25-May-2017.) |
|
''' | ||
| Theorem | funopafvb 38696 | Equivalence of function value and ordered pair membership, analogous to funopfvb 5930. (Contributed by Alexander van der Vekens, 25-May-2017.) |
|
''' | ||
| Theorem | funbrafv 38697 | The second argument of a binary relation on a function is the function's value, analogous to funbrfv 5925. (Contributed by Alexander van der Vekens, 25-May-2017.) |
|
'''
| ||
| Theorem | funbrafv2b 38698 | Function value in terms of a binary relation, analogous to funbrfv2b 5931. (Contributed by Alexander van der Vekens, 25-May-2017.) |
|
''' | ||
| Theorem | dfafn5a 38699* | Representation of a function in terms of its values, analogous to dffn5 5932 (only one direction of implication!). (Contributed by Alexander van der Vekens, 25-May-2017.) |
 ''' | ||
| Theorem | dfafn5b 38700* | Representation of a function in terms of its values, analogous to dffn5 5932 (only if it is assumed that the function value for each x is a set). (Contributed by Alexander van der Vekens, 25-May-2017.) |
|
''' ''' | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |
