Home | Metamath
Proof Explorer Theorem List (p. 61 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 | fnresdisj 6001 | A function restricted to a class disjoint with its domain is empty. (Contributed by NM, 23-Sep-2004.) |
Theorem | 2elresin 6002 | Membership in two functions restricted by each other's domain. (Contributed by NM, 8-Aug-1994.) |
Theorem | fnssresb 6003 | Restriction of a function with a subclass of its domain. (Contributed by NM, 10-Oct-2007.) |
Theorem | fnssres 6004 | Restriction of a function with a subclass of its domain. (Contributed by NM, 2-Aug-1994.) |
Theorem | fnresin1 6005 | Restriction of a function's domain with an intersection. (Contributed by NM, 9-Aug-1994.) |
Theorem | fnresin2 6006 | Restriction of a function's domain with an intersection. (Contributed by NM, 9-Aug-1994.) |
Theorem | fnres 6007* | An equivalence for functionality of a restriction. Compare dffun8 5916. (Contributed by Mario Carneiro, 20-May-2015.) |
Theorem | fnresi 6008 | Functionality and domain of restricted identity. (Contributed by NM, 27-Aug-2004.) |
Theorem | idssxp 6009 | A diagonal set as a subset of a Cartesian product. (Contributed by Thierry Arnoux, 29-Dec-2019.) |
Theorem | fnima 6010 | The image of a function's domain is its range. (Contributed by NM, 4-Nov-2004.) (Proof shortened by Andrew Salmon, 17-Sep-2011.) |
Theorem | fn0 6011 | A function with empty domain is empty. (Contributed by NM, 15-Apr-1998.) (Proof shortened by Andrew Salmon, 17-Sep-2011.) |
Theorem | fnimadisj 6012 | A class that is disjoint with the domain of a function has an empty image under the function. (Contributed by FL, 24-Jan-2007.) |
Theorem | fnimaeq0 6013 | Images under a function never map nonempty sets to empty sets. EDITORIAL: usable in fnwe2lem2 37621. (Contributed by Stefan O'Rear, 21-Jan-2015.) |
Theorem | dfmpt3 6014 | Alternate definition for the "maps to" notation df-mpt 4730. (Contributed by Mario Carneiro, 30-Dec-2016.) |
Theorem | mptfnf 6015 | The maps-to notation defines a function with domain. (Contributed by Scott Fenton, 21-Mar-2011.) (Revised by Thierry Arnoux, 10-May-2017.) |
Theorem | fnmptf 6016 | The maps-to notation defines a function with domain. (Contributed by NM, 9-Apr-2013.) (Revised by Thierry Arnoux, 10-May-2017.) |
Theorem | fnopabg 6017* | Functionality and domain of an ordered-pair class abstraction. (Contributed by NM, 30-Jan-2004.) (Proof shortened by Mario Carneiro, 4-Dec-2016.) |
Theorem | fnopab 6018* | Functionality and domain of an ordered-pair class abstraction. (Contributed by NM, 5-Mar-1996.) |
Theorem | mptfng 6019* | The maps-to notation defines a function with domain. (Contributed by Scott Fenton, 21-Mar-2011.) |
Theorem | fnmpt 6020* | The maps-to notation defines a function with domain. (Contributed by NM, 9-Apr-2013.) |
Theorem | mpt0 6021 | A mapping operation with empty domain. (Contributed by Mario Carneiro, 28-Dec-2014.) |
Theorem | fnmpti 6022* | Functionality and domain of an ordered-pair class abstraction. (Contributed by NM, 29-Jan-2004.) (Revised by Mario Carneiro, 31-Aug-2015.) |
Theorem | dmmpti 6023* | Domain of the mapping operation. (Contributed by NM, 6-Sep-2005.) (Revised by Mario Carneiro, 31-Aug-2015.) |
Theorem | dmmptd 6024* | The domain of the mapping operation, deduction form. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Theorem | mptun 6025 | Union of mappings which are mutually compatible. (Contributed by Mario Carneiro, 31-Aug-2015.) |
Theorem | feq1 6026 | Equality theorem for functions. (Contributed by NM, 1-Aug-1994.) |
Theorem | feq2 6027 | Equality theorem for functions. (Contributed by NM, 1-Aug-1994.) |
Theorem | feq3 6028 | Equality theorem for functions. (Contributed by NM, 1-Aug-1994.) |
Theorem | feq23 6029 | Equality theorem for functions. (Contributed by FL, 14-Jul-2007.) (Proof shortened by Andrew Salmon, 17-Sep-2011.) |
Theorem | feq1d 6030 | Equality deduction for functions. (Contributed by NM, 19-Feb-2008.) |
Theorem | feq2d 6031 | Equality deduction for functions. (Contributed by Paul Chapman, 22-Jun-2011.) |
Theorem | feq3d 6032 | Equality deduction for functions. (Contributed by AV, 1-Jan-2020.) |
Theorem | feq12d 6033 | Equality deduction for functions. (Contributed by Paul Chapman, 22-Jun-2011.) |
Theorem | feq123d 6034 | Equality deduction for functions. (Contributed by Paul Chapman, 22-Jun-2011.) |
Theorem | feq123 6035 | Equality theorem for functions. (Contributed by FL, 16-Nov-2008.) |
Theorem | feq1i 6036 | Equality inference for functions. (Contributed by Paul Chapman, 22-Jun-2011.) |
Theorem | feq2i 6037 | Equality inference for functions. (Contributed by NM, 5-Sep-2011.) |
Theorem | feq12i 6038 | Equality inference for functions. (Contributed by AV, 7-Feb-2021.) |
Theorem | feq23i 6039 | Equality inference for functions. (Contributed by Paul Chapman, 22-Jun-2011.) |
Theorem | feq23d 6040 | Equality deduction for functions. (Contributed by NM, 8-Jun-2013.) |
Theorem | nff 6041 | Bound-variable hypothesis builder for a mapping. (Contributed by NM, 29-Jan-2004.) (Revised by Mario Carneiro, 15-Oct-2016.) |
Theorem | sbcfng 6042* | Distribute proper substitution through the function predicate with a domain. (Contributed by Alexander van der Vekens, 15-Jul-2018.) |
Theorem | sbcfg 6043* | Distribute proper substitution through the function predicate with domain and codomain. (Contributed by Alexander van der Vekens, 15-Jul-2018.) |
Theorem | elimf 6044 | Eliminate a mapping hypothesis for the weak deduction theorem dedth 4139, when a special case is provable, in order to convert from a hypothesis to an antecedent. (Contributed by NM, 24-Aug-2006.) |
Theorem | ffn 6045 | A mapping is a function with domain. (Contributed by NM, 2-Aug-1994.) |
Theorem | ffnd 6046 | A mapping is a function with domain, deduction form. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
Theorem | dffn2 6047 | Any function is a mapping into . (Contributed by NM, 31-Oct-1995.) (Proof shortened by Andrew Salmon, 17-Sep-2011.) |
Theorem | ffun 6048 | A mapping is a function. (Contributed by NM, 3-Aug-1994.) |
Theorem | ffund 6049 | A mapping is a function, deduction version. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
Theorem | frel 6050 | A mapping is a relation. (Contributed by NM, 3-Aug-1994.) |
Theorem | fdm 6051 | The domain of a mapping. (Contributed by NM, 2-Aug-1994.) |
Theorem | fdmi 6052 | The domain of a mapping. (Contributed by NM, 28-Jul-2008.) |
Theorem | frn 6053 | The range of a mapping. (Contributed by NM, 3-Aug-1994.) |
Theorem | dffn3 6054 | A function maps to its range. (Contributed by NM, 1-Sep-1999.) |
Theorem | ffrn 6055 | A function maps to its range. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
Theorem | fss 6056 | Expanding the codomain of a mapping. (Contributed by NM, 10-May-1998.) (Proof shortened by Andrew Salmon, 17-Sep-2011.) |
Theorem | fssd 6057 | Expanding the codomain of a mapping, deduction form. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Theorem | fco 6058 | Composition of two mappings. (Contributed by NM, 29-Aug-1999.) (Proof shortened by Andrew Salmon, 17-Sep-2011.) |
Theorem | fco2 6059 | Functionality of a composition with weakened out of domain condition on the first argument. (Contributed by Stefan O'Rear, 11-Mar-2015.) |
Theorem | fssxp 6060 | A mapping is a class of ordered pairs. (Contributed by NM, 3-Aug-1994.) (Proof shortened by Andrew Salmon, 17-Sep-2011.) |
Theorem | funssxp 6061 | Two ways of specifying a partial function from to . (Contributed by NM, 13-Nov-2007.) |
Theorem | ffdm 6062 | A mapping is a partial function. (Contributed by NM, 25-Nov-2007.) |
Theorem | ffdmd 6063 | The domain of a function. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
Theorem | fdmrn 6064 | A different way to write is a function. (Contributed by Thierry Arnoux, 7-Dec-2016.) |
Theorem | opelf 6065 | The members of an ordered pair element of a mapping belong to the mapping's domain and codomain. (Contributed by NM, 10-Dec-2003.) (Revised by Mario Carneiro, 26-Apr-2015.) |
Theorem | fun 6066 | The union of two functions with disjoint domains. (Contributed by NM, 22-Sep-2004.) |
Theorem | fun2 6067 | The union of two functions with disjoint domains. (Contributed by Mario Carneiro, 12-Mar-2015.) |
Theorem | fun2d 6068 | The union of functions with disjoint domains is a function, deduction version of fun2 6067. (Contributed by AV, 11-Oct-2020.) (Revised by AV, 24-Oct-2021.) |
Theorem | fnfco 6069 | Composition of two functions. (Contributed by NM, 22-May-2006.) |
Theorem | fssres 6070 | Restriction of a function with a subclass of its domain. (Contributed by NM, 23-Sep-2004.) |
Theorem | fssresd 6071 | Restriction of a function with a subclass of its domain, deduction form. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Theorem | fssres2 6072 | Restriction of a restricted function with a subclass of its domain. (Contributed by NM, 21-Jul-2005.) |
Theorem | fresin 6073 | An identity for the mapping relationship under restriction. (Contributed by Scott Fenton, 4-Sep-2011.) (Proof shortened by Mario Carneiro, 26-May-2016.) |
Theorem | resasplit 6074 | If two functions agree on their common domain, express their union as a union of three functions with pairwise disjoint domains. (Contributed by Stefan O'Rear, 9-Oct-2014.) |
Theorem | fresaun 6075 | The union of two functions which agree on their common domain is a function. (Contributed by Stefan O'Rear, 9-Oct-2014.) |
Theorem | fresaunres2 6076 | From the union of two functions that agree on the domain overlap, either component can be recovered by restriction. (Contributed by Stefan O'Rear, 9-Oct-2014.) |
Theorem | fresaunres1 6077 | From the union of two functions that agree on the domain overlap, either component can be recovered by restriction. (Contributed by Mario Carneiro, 16-Feb-2015.) |
Theorem | fcoi1 6078 | Composition of a mapping and restricted identity. (Contributed by NM, 13-Dec-2003.) (Proof shortened by Andrew Salmon, 17-Sep-2011.) |
Theorem | fcoi2 6079 | Composition of restricted identity and a mapping. (Contributed by NM, 13-Dec-2003.) (Proof shortened by Andrew Salmon, 17-Sep-2011.) |
Theorem | feu 6080* | There is exactly one value of a function in its codomain. (Contributed by NM, 10-Dec-2003.) |
Theorem | fimass 6081 | The image of a class is a subset of its codomain. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
Theorem | fcnvres 6082 | The converse of a restriction of a function. (Contributed by NM, 26-Mar-1998.) |
Theorem | fimacnvdisj 6083 | The preimage of a class disjoint with a mapping's codomain is empty. (Contributed by FL, 24-Jan-2007.) |
Theorem | fint 6084* | Function into an intersection. (Contributed by NM, 14-Oct-1999.) (Proof shortened by Andrew Salmon, 17-Sep-2011.) |
Theorem | fin 6085 | Mapping into an intersection. (Contributed by NM, 14-Sep-1999.) (Proof shortened by Andrew Salmon, 17-Sep-2011.) |
Theorem | f0 6086 | The empty function. (Contributed by NM, 14-Aug-1999.) |
Theorem | f00 6087 | A class is a function with empty codomain iff it and its domain are empty. (Contributed by NM, 10-Dec-2003.) |
Theorem | f0bi 6088 | A function with empty domain is empty. (Contributed by Alexander van der Vekens, 30-Jun-2018.) |
Theorem | f0dom0 6089 | A function is empty iff it has an empty domain. (Contributed by AV, 10-Feb-2019.) |
Theorem | f0rn0 6090* | If there is no element in the range of a function, its domain must be empty. (Contributed by Alexander van der Vekens, 12-Jul-2018.) |
Theorem | fconst 6091 | A Cartesian product with a singleton is a constant function. (Contributed by NM, 14-Aug-1999.) (Proof shortened by Andrew Salmon, 17-Sep-2011.) |
Theorem | fconstg 6092 | A Cartesian product with a singleton is a constant function. (Contributed by NM, 19-Oct-2004.) |
Theorem | fnconstg 6093 | A Cartesian product with a singleton is a constant function. (Contributed by NM, 24-Jul-2014.) |
Theorem | fconst6g 6094 | Constant function with loose range. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
Theorem | fconst6 6095 | A constant function as a mapping. (Contributed by Jeff Madsen, 30-Nov-2009.) (Revised by Mario Carneiro, 22-Apr-2015.) |
Theorem | f1eq1 6096 | Equality theorem for one-to-one functions. (Contributed by NM, 10-Feb-1997.) |
Theorem | f1eq2 6097 | Equality theorem for one-to-one functions. (Contributed by NM, 10-Feb-1997.) |
Theorem | f1eq3 6098 | Equality theorem for one-to-one functions. (Contributed by NM, 10-Feb-1997.) |
Theorem | nff1 6099 | Bound-variable hypothesis builder for a one-to-one function. (Contributed by NM, 16-May-2004.) |
Theorem | dff12 6100* | Alternate definition of a one-to-one function. (Contributed by NM, 31-Dec-1996.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |