Home | Metamath
Proof Explorer Theorem List (p. 65 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 | fcoconst 6401 | Composition with a constant function. (Contributed by Stefan O'Rear, 11-Mar-2015.) |
Theorem | fsn 6402 | A function maps a singleton to a singleton iff it is the singleton of an ordered pair. (Contributed by NM, 10-Dec-2003.) |
Theorem | fsn2 6403 | A function that maps a singleton to a class is the singleton of an ordered pair. (Contributed by NM, 19-May-2004.) |
Theorem | fsng 6404 | A function maps a singleton to a singleton iff it is the singleton of an ordered pair. (Contributed by NM, 26-Oct-2012.) |
Theorem | fsn2g 6405 | A function that maps a singleton to a class is the singleton of an ordered pair. (Contributed by Thierry Arnoux, 11-Jul-2020.) |
Theorem | xpsng 6406 | The Cartesian product of two singletons. (Contributed by Mario Carneiro, 30-Apr-2015.) |
Theorem | xpsn 6407 | The Cartesian product of two singletons. (Contributed by NM, 4-Nov-2006.) |
Theorem | f1o2sn 6408 | A singleton with a nested ordered pair is a one-to-one function of the cartesian product of two singleton onto a singleton. (Contributed by AV, 15-Aug-2019.) |
Theorem | residpr 6409 | Restriction of the identity to a pair. (Contributed by AV, 11-Dec-2018.) |
Theorem | dfmpt 6410 | Alternate definition for the "maps to" notation df-mpt 4730 (although it requires that be a set). (Contributed by NM, 24-Aug-2010.) (Revised by Mario Carneiro, 30-Dec-2016.) |
Theorem | fnasrn 6411 | A function expressed as the range of another function. (Contributed by Mario Carneiro, 22-Jun-2013.) (Proof shortened by Mario Carneiro, 31-Aug-2015.) |
Theorem | funiun 6412* | A function is a union of singletons of ordered pairs indexed by its domain. (Contributed by AV, 18-Sep-2020.) |
Theorem | funopsn 6413* | If a function is an ordered pair then it is a singleton of an ordered pair. (Contributed by AV, 20-Sep-2020.) |
Theorem | funop 6414* | An ordered pair is a function iff it is a singleton of an ordered pair. (Contributed by AV, 20-Sep-2020.) |
Theorem | funopdmsn 6415 | The domain of a function which is an ordered pair is a singleton. (Contributed by AV, 15-Nov-2021.) |
Theorem | funsndifnop 6416 | A singleton of an ordered pair is not an ordered pair if the components are different. (Contributed by AV, 23-Sep-2020.) |
Theorem | funsneqopsn 6417 | A singleton of an ordered pair is an ordered pair of equal singletons if the components are equal. (Contributed by AV, 24-Sep-2020.) |
Theorem | funsneqop 6418 | A singleton of an ordered pair is an ordered pair if the components are equal. (Contributed by AV, 24-Sep-2020.) |
Theorem | funsneqopb 6419 | A singleton of an ordered pair is an ordered pair iff the components are equal. (Contributed by AV, 24-Sep-2020.) |
Theorem | ressnop0 6420 | If is not in , then the restriction of a singleton of to is null. (Contributed by Scott Fenton, 15-Apr-2011.) |
Theorem | fpr 6421 | A function with a domain of two elements. (Contributed by Jeff Madsen, 20-Jun-2010.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) |
Theorem | fprg 6422 | A function with a domain of two elements. (Contributed by FL, 2-Feb-2014.) |
Theorem | ftpg 6423 | A function with a domain of three elements. (Contributed by Alexander van der Vekens, 4-Dec-2017.) |
Theorem | ftp 6424 | A function with a domain of three elements. (Contributed by Stefan O'Rear, 17-Oct-2014.) (Proof shortened by Alexander van der Vekens, 23-Jan-2018.) |
Theorem | fnressn 6425 | A function restricted to a singleton. (Contributed by NM, 9-Oct-2004.) |
Theorem | funressn 6426 | A function restricted to a singleton. (Contributed by Mario Carneiro, 16-Nov-2014.) |
Theorem | fressnfv 6427 | The value of a function restricted to a singleton. (Contributed by NM, 9-Oct-2004.) |
Theorem | fvrnressn 6428 | If the value of a function is in the range of the function restricted to the singleton containing the argument, then the value of the function is in the range of the function. (Contributed by Alexander van der Vekens, 22-Jul-2018.) |
Theorem | fvressn 6429 | The value of a function restricted to the singleton containing the argument equals the value of the function for this argument. (Contributed by Alexander van der Vekens, 22-Jul-2018.) |
Theorem | fvn0fvelrn 6430 | If the value of a function is not null, the value is an element of the range of the function. (Contributed by Alexander van der Vekens, 22-Jul-2018.) |
Theorem | fvconst 6431 | The value of a constant function. (Contributed by NM, 30-May-1999.) |
Theorem | fnsnb 6432 | A function whose domain is a singleton can be represented as a singleton of an ordered pair. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) Revised to add reverse implication. (Revised by NM, 29-Dec-2018.) |
Theorem | fmptsn 6433* | Express a singleton function in maps-to notation. (Contributed by NM, 6-Jun-2006.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) (Revised by Stefan O'Rear, 28-Feb-2015.) |
Theorem | fmptsng 6434* | Express a singleton function in maps-to notation. Version of fmptsn 6433 allowing the mapping value to depend on the mapping variable (usual case). (Contributed by AV, 27-Feb-2019.) |
Theorem | fmptsnd 6435* | Express a singleton function in maps-to notation. Deduction form of fmptsng 6434. (Contributed by AV, 4-Aug-2019.) |
Theorem | fmptap 6436* | Append an additional value to a function. (Contributed by NM, 6-Jun-2006.) (Revised by Mario Carneiro, 31-Aug-2015.) |
Theorem | fmptapd 6437* | Append an additional value to a function. (Contributed by Thierry Arnoux, 3-Jan-2017.) |
Theorem | fmptpr 6438* | Express a pair function in maps-to notation. (Contributed by Thierry Arnoux, 3-Jan-2017.) |
Theorem | fvresi 6439 | The value of a restricted identity function. (Contributed by NM, 19-May-2004.) |
Theorem | fninfp 6440* | Express the class of fixed points of a function. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
Theorem | fnelfp 6441 | Property of a fixed point of a function. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
Theorem | fndifnfp 6442* | Express the class of non-fixed points of a function. (Contributed by Stefan O'Rear, 14-Aug-2015.) |
Theorem | fnelnfp 6443 | Property of a non-fixed point of a function. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
Theorem | fnnfpeq0 6444 | A function is the identity iff it moves no points. (Contributed by Stefan O'Rear, 25-Aug-2015.) |
Theorem | fvunsn 6445 | Remove an ordered pair not participating in a function value. (Contributed by NM, 1-Oct-2013.) (Revised by Mario Carneiro, 28-May-2014.) |
Theorem | fvsn 6446 | The value of a singleton of an ordered pair is the second member. (Contributed by NM, 12-Aug-1994.) |
Theorem | fvsng 6447 | The value of a singleton of an ordered pair is the second member. (Contributed by NM, 26-Oct-2012.) |
Theorem | fvsnun1 6448 | The value of a function with one of its ordered pairs replaced, at the replaced ordered pair. See also fvsnun2 6449. (Contributed by NM, 23-Sep-2007.) |
Theorem | fvsnun2 6449 | The value of a function with one of its ordered pairs replaced, at arguments other than the replaced one. See also fvsnun1 6448. (Contributed by NM, 23-Sep-2007.) |
Theorem | fnsnsplit 6450 | Split a function into a single point and all the rest. (Contributed by Stefan O'Rear, 27-Feb-2015.) |
Theorem | fsnunf 6451 | Adjoining a point to a function gives a function. (Contributed by Stefan O'Rear, 28-Feb-2015.) |
Theorem | fsnunf2 6452 | Adjoining a point to a punctured function gives a function. (Contributed by Stefan O'Rear, 28-Feb-2015.) |
Theorem | fsnunfv 6453 | Recover the added point from a point-added function. (Contributed by Stefan O'Rear, 28-Feb-2015.) (Revised by NM, 18-May-2017.) |
Theorem | fsnunres 6454 | Recover the original function from a point-added function. (Contributed by Stefan O'Rear, 28-Feb-2015.) |
Theorem | funresdfunsn 6455 | Restricting a function to a domain without one element of the domain of the function, and adding a pair of this element and the function value of the element results in the function itself. (Contributed by AV, 2-Dec-2018.) |
Theorem | fvpr1 6456 | The value of a function with a domain of two elements. (Contributed by Jeff Madsen, 20-Jun-2010.) |
Theorem | fvpr2 6457 | The value of a function with a domain of two elements. (Contributed by Jeff Madsen, 20-Jun-2010.) |
Theorem | fvpr1g 6458 | The value of a function with a domain of (at most) two elements. (Contributed by Alexander van der Vekens, 3-Dec-2017.) |
Theorem | fvpr2g 6459 | The value of a function with a domain of (at most) two elements. (Contributed by Alexander van der Vekens, 3-Dec-2017.) |
Theorem | fvtp1 6460 | The first value of a function with a domain of three elements. (Contributed by NM, 14-Sep-2011.) |
Theorem | fvtp2 6461 | The second value of a function with a domain of three elements. (Contributed by NM, 14-Sep-2011.) |
Theorem | fvtp3 6462 | The third value of a function with a domain of three elements. (Contributed by NM, 14-Sep-2011.) |
Theorem | fvtp1g 6463 | The value of a function with a domain of (at most) three elements. (Contributed by Alexander van der Vekens, 4-Dec-2017.) |
Theorem | fvtp2g 6464 | The value of a function with a domain of (at most) three elements. (Contributed by Alexander van der Vekens, 4-Dec-2017.) |
Theorem | fvtp3g 6465 | The value of a function with a domain of (at most) three elements. (Contributed by Alexander van der Vekens, 4-Dec-2017.) |
Theorem | tpres 6466 | An unordered triple of ordered pairs restricted to all but one first components of the pairs is an unordered pair of ordered pairs. (Contributed by AV, 14-Mar-2020.) |
Theorem | fvconst2g 6467 | The value of a constant function. (Contributed by NM, 20-Aug-2005.) |
Theorem | fconst2g 6468 | A constant function expressed as a Cartesian product. (Contributed by NM, 27-Nov-2007.) |
Theorem | fvconst2 6469 | The value of a constant function. (Contributed by NM, 16-Apr-2005.) |
Theorem | fconst2 6470 | A constant function expressed as a Cartesian product. (Contributed by NM, 20-Aug-1999.) |
Theorem | fconst5 6471 | Two ways to express that a function is constant. (Contributed by NM, 27-Nov-2007.) |
Theorem | fnprb 6472 | A function whose domain has at most two elements can be represented as a set of at most two ordered pairs. (Contributed by FL, 26-Jun-2011.) (Proof shortened by Scott Fenton, 12-Oct-2017.) Revised to eliminate unnecessary antecedent . (Revised by NM, 29-Dec-2018.) |
Theorem | fntpb 6473 | A function whose domain has at most three elements can be represented as a set of at most three ordered pairs. (Contributed by AV, 26-Jan-2021.) |
Theorem | fnpr2g 6474 | A function whose domain has at most two elements can be represented as a set of at most two ordered pairs. (Contributed by Thierry Arnoux, 12-Jul-2020.) |
Theorem | fpr2g 6475 | A function that maps a pair to a class is a pair of ordered pairs. (Contributed by Thierry Arnoux, 12-Jul-2020.) |
Theorem | fconstfv 6476* | A constant function expressed in terms of its functionality, domain, and value. See also fconst2 6470. (Contributed by NM, 27-Aug-2004.) (Proof shortened by OpenAI, 25-Mar-2020.) |
Theorem | fconst3 6477 | Two ways to express a constant function. (Contributed by NM, 15-Mar-2007.) |
Theorem | fconst4 6478 | Two ways to express a constant function. (Contributed by NM, 8-Mar-2007.) |
Theorem | resfunexg 6479 | The restriction of a function to a set exists. Compare Proposition 6.17 of [TakeutiZaring] p. 28. (Contributed by NM, 7-Apr-1995.) (Revised by Mario Carneiro, 22-Jun-2013.) |
Theorem | resiexd 6480 | The restriction of the identity relation to a set is a set. (Contributed by AV, 15-Feb-2020.) |
Theorem | fnex 6481 | If the domain of a function is a set, the function is a set. Theorem 6.16(1) of [TakeutiZaring] p. 28. This theorem is derived using the Axiom of Replacement in the form of resfunexg 6479. See fnexALT 7132 for alternate proof. (Contributed by NM, 14-Aug-1994.) (Proof shortened by Andrew Salmon, 17-Sep-2011.) |
Theorem | funex 6482 | If the domain of a function exists, so the function. Part of Theorem 4.15(v) of [Monk1] p. 46. This theorem is derived using the Axiom of Replacement in the form of fnex 6481. (Note: Any resemblance between F.U.N.E.X. and "Have You Any Eggs" is purely a coincidence originated by Swedish chefs.) (Contributed by NM, 11-Nov-1995.) |
Theorem | opabex 6483* | Existence of a function expressed as class of ordered pairs. (Contributed by NM, 21-Jul-1996.) |
Theorem | mptexg 6484* | If the domain of a function given by maps-to notation is a set, the function is a set. (Contributed by FL, 6-Jun-2011.) (Revised by Mario Carneiro, 31-Aug-2015.) |
Theorem | mptexgf 6485 | If the domain of a function given by maps-to notation is a set, the function is a set. (Contributed by FL, 6-Jun-2011.) (Revised by Mario Carneiro, 31-Aug-2015.) (Revised by Thierry Arnoux, 17-May-2020.) |
Theorem | mptex 6486* | If the domain of a function given by maps-to notation is a set, the function is a set. Inference version of mptexg 6484. (Contributed by NM, 22-Apr-2005.) (Revised by Mario Carneiro, 20-Dec-2013.) |
Theorem | mptexd 6487* | If the domain of a function given by maps-to notation is a set, the function is a set. Deduction version of mptexg 6484. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
Theorem | mptrabex 6488* | If the domain of a function given by maps-to notation is a class abstraction based on a set, the function is a set. (Contributed by AV, 16-Jul-2019.) (Revised by AV, 26-Mar-2021.) |
Theorem | mptrabexOLD 6489* | Obsolete version of mptrabex 6488 as of 26-Mar-2021. (Contributed by AV, 16-Jul-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | fex 6490 | If the domain of a mapping is a set, the function is a set. (Contributed by NM, 3-Oct-1999.) |
Theorem | eufnfv 6491* | A function is uniquely determined by its values. (Contributed by NM, 31-Aug-2011.) |
Theorem | funfvima 6492 | A function's value in a preimage belongs to the image. (Contributed by NM, 23-Sep-2003.) |
Theorem | funfvima2 6493 | A function's value in an included preimage belongs to the image. (Contributed by NM, 3-Feb-1997.) |
Theorem | resfvresima 6494 | The value of the function value of a restriction for a function restricted to the image of the restricting subset. (Contributed by AV, 6-Mar-2021.) |
Theorem | funfvima3 6495 | A class including a function contains the function's value in the image of the singleton of the argument. (Contributed by NM, 23-Mar-2004.) |
Theorem | fnfvima 6496 | The function value of an operand in a set is contained in the image of that set, using the abbreviation. (Contributed by Stefan O'Rear, 10-Mar-2015.) |
Theorem | rexima 6497* | Existential quantification under an image in terms of the base set. (Contributed by Stefan O'Rear, 21-Jan-2015.) |
Theorem | ralima 6498* | Universal quantification under an image in terms of the base set. (Contributed by Stefan O'Rear, 21-Jan-2015.) |
Theorem | idref 6499* |
TODO: This is the same as issref 5509 (which has a much longer proof).
Should we replace issref 5509 with this one? - NM 9-May-2016.
Two ways to state a relation is reflexive. (Adapted from Tarski.) (Contributed by FL, 15-Jan-2012.) (Proof shortened by Mario Carneiro, 3-Nov-2015.) (Proof modification is discouraged.) |
Theorem | fvclss 6500* | Upper bound for the class of values of a class. (Contributed by NM, 9-Nov-1995.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |