Home | Metamath
Proof Explorer Theorem List (p. 64 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 | fvmptf 6301* | Value of a function given by an ordered-pair class abstraction. This version of fvmptg 6280 uses bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 8-Nov-2005.) (Revised by Mario Carneiro, 15-Oct-2016.) |
Theorem | fvmptnf 6302* | The value of a function given by an ordered-pair class abstraction is the empty set when the class it would otherwise map to is a proper class. This version of fvmptn 6303 uses bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 21-Oct-2003.) (Revised by Mario Carneiro, 11-Sep-2015.) |
Theorem | fvmptn 6303* | This somewhat non-intuitive theorem tells us the value of its function is the empty set when the class it would otherwise map to is a proper class. This is a technical lemma that can help eliminate redundant sethood antecedents otherwise required by fvmptg 6280. (Contributed by NM, 21-Oct-2003.) (Revised by Mario Carneiro, 9-Sep-2013.) |
Theorem | fvmptss2 6304* | A mapping always evaluates to a subset of the substituted expression in the mapping, even if this is a proper class, or we are out of the domain. (Contributed by Mario Carneiro, 13-Feb-2015.) |
Theorem | elfvmptrab1 6305* | Implications for the value of a function defined by the maps-to notation with a class abstraction as a result having an element. Here, the base set of the class abstraction depends on the argument of the function. (Contributed by Alexander van der Vekens, 15-Jul-2018.) |
Theorem | elfvmptrab 6306* | Implications for the value of a function defined by the maps-to notation with a class abstraction as a result having an element. (Contributed by Alexander van der Vekens, 15-Jul-2018.) |
Theorem | fvopab4ndm 6307* | Value of a function given by an ordered-pair class abstraction, outside of its domain. (Contributed by NM, 28-Mar-2008.) |
Theorem | fvmptndm 6308* | Value of a function given by the "maps to" notation, outside of its domain. (Contributed by AV, 31-Dec-2020.) |
Theorem | fvopab5 6309* | The value of a function that is expressed as an ordered pair abstraction. (Contributed by NM, 19-Feb-2006.) (Revised by Mario Carneiro, 11-Sep-2015.) |
Theorem | fvopab6 6310* | Value of a function given by ordered-pair class abstraction. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 11-Sep-2015.) |
Theorem | eqfnfv 6311* | Equality of functions is determined by their values. Special case of Exercise 4 of [TakeutiZaring] p. 28 (with domain equality omitted). (Contributed by NM, 3-Aug-1994.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) (Proof shortened by Mario Carneiro, 31-Aug-2015.) |
Theorem | eqfnfv2 6312* | Equality of functions is determined by their values. Exercise 4 of [TakeutiZaring] p. 28. (Contributed by NM, 3-Aug-1994.) (Revised by Mario Carneiro, 31-Aug-2015.) |
Theorem | eqfnfv3 6313* | Derive equality of functions from equality of their values. (Contributed by Jeff Madsen, 2-Sep-2009.) |
Theorem | eqfnfvd 6314* | Deduction for equality of functions. (Contributed by Mario Carneiro, 24-Jul-2014.) |
Theorem | eqfnfv2f 6315* | Equality of functions is determined by their values. Special case of Exercise 4 of [TakeutiZaring] p. 28 (with domain equality omitted). This version of eqfnfv 6311 uses bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 29-Jan-2004.) |
Theorem | eqfunfv 6316* | Equality of functions is determined by their values. (Contributed by Scott Fenton, 19-Jun-2011.) |
Theorem | fvreseq0 6317* | Equality of restricted functions is determined by their values (for functions with different domains). (Contributed by AV, 6-Jan-2019.) |
Theorem | fvreseq1 6318* | Equality of a function restricted to the domain of another function. (Contributed by AV, 6-Jan-2019.) |
Theorem | fvreseq 6319* | Equality of restricted functions is determined by their values. (Contributed by NM, 3-Aug-1994.) (Prove shortened by AV, 4-Mar-2019.) |
Theorem | fnmptfvd 6320* | A function with a given domain is a mapping defined by its function values. (Contributed by AV, 1-Mar-2019.) |
Theorem | fndmdif 6321* | Two ways to express the locus of differences between two functions. (Contributed by Stefan O'Rear, 17-Jan-2015.) |
Theorem | fndmdifcom 6322 | The difference set between two functions is commutative. (Contributed by Stefan O'Rear, 17-Jan-2015.) |
Theorem | fndmdifeq0 6323 | The difference set of two functions is empty if and only if the functions are equal. (Contributed by Stefan O'Rear, 17-Jan-2015.) |
Theorem | fndmin 6324* | Two ways to express the locus of equality between two functions. (Contributed by Stefan O'Rear, 17-Jan-2015.) |
Theorem | fneqeql 6325 | Two functions are equal iff their equalizer is the whole domain. (Contributed by Stefan O'Rear, 7-Mar-2015.) |
Theorem | fneqeql2 6326 | Two functions are equal iff their equalizer contains the whole domain. (Contributed by Stefan O'Rear, 9-Mar-2015.) |
Theorem | fnreseql 6327 | Two functions are equal on a subset iff their equalizer contains that subset. (Contributed by Stefan O'Rear, 7-Mar-2015.) |
Theorem | chfnrn 6328* | The range of a choice function (a function that chooses an element from each member of its domain) is included in the union of its domain. (Contributed by NM, 31-Aug-1999.) |
Theorem | funfvop 6329 | Ordered pair with function value. Part of Theorem 4.3(i) of [Monk1] p. 41. (Contributed by NM, 14-Oct-1996.) |
Theorem | funfvbrb 6330 | Two ways to say that is in the domain of . (Contributed by Mario Carneiro, 1-May-2014.) |
Theorem | fvimacnvi 6331 | A member of a preimage is a function value argument. (Contributed by NM, 4-May-2007.) |
Theorem | fvimacnv 6332 | The argument of a function value belongs to the preimage of any class containing the function value. Raph Levien remarks: "This proof is unsatisfying, because it seems to me that funimass2 5972 could probably be strengthened to a biconditional." (Contributed by Raph Levien, 20-Nov-2006.) |
Theorem | funimass3 6333 | A kind of contraposition law that infers an image subclass from a subclass of a preimage. Raph Levien remarks: "Likely this could be proved directly, and fvimacnv 6332 would be the special case of being a singleton, but it works this way round too." (Contributed by Raph Levien, 20-Nov-2006.) |
Theorem | funimass5 6334* | A subclass of a preimage in terms of function values. (Contributed by NM, 15-May-2007.) |
Theorem | funconstss 6335* | Two ways of specifying that a function is constant on a subdomain. (Contributed by NM, 8-Mar-2007.) |
Theorem | fvimacnvALT 6336 | Alternate proof of fvimacnv 6332, based on funimass3 6333. If funimass3 6333 is ever proved directly, as opposed to using funimacnv 5970 pointwise, then the proof of funimacnv 5970 should be replaced with this one. (Contributed by Raph Levien, 20-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | elpreima 6337 | Membership in the preimage of a set under a function. (Contributed by Jeff Madsen, 2-Sep-2009.) |
Theorem | fniniseg 6338 | Membership in the preimage of a singleton, under a function. (Contributed by Mario Carneiro, 12-May-2014.) (Proof shortened by Mario Carneiro , 28-Apr-2015.) |
Theorem | fncnvima2 6339* | Inverse images under functions expressed as abstractions. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
Theorem | fniniseg2 6340* | Inverse point images under functions expressed as abstractions. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
Theorem | unpreima 6341 | Preimage of a union. (Contributed by Jeff Madsen, 2-Sep-2009.) |
Theorem | inpreima 6342 | Preimage of an intersection. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 14-Jun-2016.) |
Theorem | difpreima 6343 | Preimage of a difference. (Contributed by Mario Carneiro, 14-Jun-2016.) |
Theorem | respreima 6344 | The preimage of a restricted function. (Contributed by Jeff Madsen, 2-Sep-2009.) |
Theorem | iinpreima 6345* | Preimage of an intersection. (Contributed by FL, 16-Apr-2012.) |
Theorem | intpreima 6346* | Preimage of an intersection. (Contributed by FL, 28-Apr-2012.) |
Theorem | fimacnv 6347 | The preimage of the codomain of a mapping is the mapping's domain. (Contributed by FL, 25-Jan-2007.) |
Theorem | fimacnvinrn 6348 | Taking the converse image of a set can be limited to the range of the function used. (Contributed by Thierry Arnoux, 21-Jan-2017.) |
Theorem | fimacnvinrn2 6349 | Taking the converse image of a set can be limited to the range of the function used. (Contributed by Thierry Arnoux, 17-Feb-2017.) |
Theorem | fvn0ssdmfun 6350* | If a class' function values for certain arguments is not the empty set, the arguments are contained in the domain of the class, and the class restricted to the arguments is a function, analogous to fvfundmfvn0 6226. (Contributed by AV, 27-Jan-2020.) |
Theorem | fnopfv 6351 | Ordered pair with function value. Part of Theorem 4.3(i) of [Monk1] p. 41. (Contributed by NM, 30-Sep-2004.) |
Theorem | fvelrn 6352 | A function's value belongs to its range. (Contributed by NM, 14-Oct-1996.) |
Theorem | nelrnfvne 6353 | A function value cannot be any element not contained in the range of the function. (Contributed by AV, 28-Jan-2020.) |
Theorem | fveqdmss 6354* | If the empty set is not contained in the range of a function, and the function values of another class (not necessarily a function) are equal to the function values of the function for all elements of the domain of the function, then the domain of the function is contained in the domain of the class. (Contributed by AV, 28-Jan-2020.) |
Theorem | fveqressseq 6355* | If the empty set is not contained in the range of a function, and the function values of another class (not necessarily a function) are equal to the function values of the function for all elements of the domain of the function, then the class restricted to the domain of the function is the function itself. (Contributed by AV, 28-Jan-2020.) |
Theorem | fnfvelrn 6356 | A function's value belongs to its range. (Contributed by NM, 15-Oct-1996.) |
Theorem | ffvelrn 6357 | A function's value belongs to its codomain. (Contributed by NM, 12-Aug-1999.) |
Theorem | ffvelrni 6358 | A function's value belongs to its codomain. (Contributed by NM, 6-Apr-2005.) |
Theorem | ffvelrnda 6359 | A function's value belongs to its codomain. (Contributed by Mario Carneiro, 29-Dec-2016.) |
Theorem | ffvelrnd 6360 | A function's value belongs to its codomain. (Contributed by Mario Carneiro, 29-Dec-2016.) |
Theorem | rexrn 6361* | Restricted existential quantification over the range of a function. (Contributed by Mario Carneiro, 24-Dec-2013.) (Revised by Mario Carneiro, 20-Aug-2014.) |
Theorem | ralrn 6362* | Restricted universal quantification over the range of a function. (Contributed by Mario Carneiro, 24-Dec-2013.) (Revised by Mario Carneiro, 20-Aug-2014.) |
Theorem | elrnrexdm 6363* | For any element in the range of a function there is an element in the domain of the function for which the function value is the element of the range. (Contributed by Alexander van der Vekens, 8-Dec-2017.) |
Theorem | elrnrexdmb 6364* | For any element in the range of a function there is an element in the domain of the function for which the function value is the element of the range. (Contributed by Alexander van der Vekens, 17-Dec-2017.) |
Theorem | eldmrexrn 6365* | For any element in the domain of a function there is an element in the range of the function which is the function value for the element of the domain. (Contributed by Alexander van der Vekens, 8-Dec-2017.) |
Theorem | eldmrexrnb 6366* | For any element in the domain of a function, there is an element in the range of the function which is the value of the function at that element. Because of the definition df-fv 5896 of the value of a function, the theorem is only valid in general if the empty set is not contained in the range of the function (the implication "to the right" is always valid). Indeed, with the definition df-fv 5896 of the value of a function, may mean that the value of at is the empty set or that is not defined at . (Contributed by Alexander van der Vekens, 17-Dec-2017.) |
Theorem | fvcofneq 6367* | The values of two function compositions are equal if the values of the composed functions are pairwise equal. (Contributed by AV, 26-Jan-2019.) |
Theorem | ralrnmpt 6368* | A restricted quantifier over an image set. (Contributed by Mario Carneiro, 20-Aug-2015.) |
Theorem | rexrnmpt 6369* | A restricted quantifier over an image set. (Contributed by Mario Carneiro, 20-Aug-2015.) |
Theorem | f0cli 6370 | Unconditional closure of a function when the range includes the empty set. (Contributed by Mario Carneiro, 12-Sep-2013.) |
Theorem | dff2 6371 | Alternate definition of a mapping. (Contributed by NM, 14-Nov-2007.) |
Theorem | dff3 6372* | Alternate definition of a mapping. (Contributed by NM, 20-Mar-2007.) |
Theorem | dff4 6373* | Alternate definition of a mapping. (Contributed by NM, 20-Mar-2007.) |
Theorem | dffo3 6374* | An onto mapping expressed in terms of function values. (Contributed by NM, 29-Oct-2006.) |
Theorem | dffo4 6375* | Alternate definition of an onto mapping. (Contributed by NM, 20-Mar-2007.) |
Theorem | dffo5 6376* | Alternate definition of an onto mapping. (Contributed by NM, 20-Mar-2007.) |
Theorem | exfo 6377* | A relation equivalent to the existence of an onto mapping. The right-hand is not necessarily a function. (Contributed by NM, 20-Mar-2007.) |
Theorem | foelrn 6378* | Property of a surjective function. (Contributed by Jeff Madsen, 4-Jan-2011.) |
Theorem | foco2 6379 | If a composition of two functions is surjective, then the function on the left is surjective. (Contributed by Jeff Madsen, 16-Jun-2011.) (Proof shortened by JJ, 14-Jul-2021.) |
Theorem | foco2OLD 6380 | Obsolete proof of foco2 6379 as of 14-Jul-2021. (Contributed by Jeff Madsen, 16-Jun-2011.) (New usage is discouraged.) (Proof modification is discouraged.) |
Theorem | fmpt 6381* | Functionality of the mapping operation. (Contributed by Mario Carneiro, 26-Jul-2013.) (Revised by Mario Carneiro, 31-Aug-2015.) |
Theorem | f1ompt 6382* | Express bijection for a mapping operation. (Contributed by Mario Carneiro, 30-May-2015.) (Revised by Mario Carneiro, 4-Dec-2016.) |
Theorem | fmpti 6383* | Functionality of the mapping operation. (Contributed by NM, 19-Mar-2005.) (Revised by Mario Carneiro, 1-Sep-2015.) |
Theorem | mptex2 6384* | If a class given as a map-to notation is a set, it's image values are set. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Theorem | fmptd 6385* | Domain and codomain of the mapping operation; deduction form. (Contributed by Mario Carneiro, 13-Jan-2013.) |
Theorem | fmpt3d 6386* | Domain and co-domain of the mapping operation; deduction form. (Contributed by Thierry Arnoux, 4-Jun-2017.) |
Theorem | fmptdf 6387* | A version of fmptd 6385 using bound-variable hypothesis instead of a distinct variable condition for . (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
Theorem | ffnfv 6388* | A function maps to a class to which all values belong. (Contributed by NM, 3-Dec-2003.) |
Theorem | ffnfvf 6389 | A function maps to a class to which all values belong. This version of ffnfv 6388 uses bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 28-Sep-2006.) |
Theorem | fnfvrnss 6390* | An upper bound for range determined by function values. (Contributed by NM, 8-Oct-2004.) |
Theorem | frnssb 6391* | A function is a function into a subset of its codomain if all of its values are elements of this subset. (Contributed by AV, 7-Feb-2021.) |
Theorem | rnmptss 6392* | The range of an operation given by the "maps to" notation as a subset. (Contributed by Thierry Arnoux, 24-Sep-2017.) |
Theorem | fmpt2d 6393* | Domain and codomain of the mapping operation; deduction form. (Contributed by NM, 27-Dec-2014.) |
Theorem | ffvresb 6394* | A necessary and sufficient condition for a restricted function. (Contributed by Mario Carneiro, 14-Nov-2013.) |
Theorem | f1oresrab 6395* | Build a bijection between restricted abstract builders, given a bijection between the base classes, deduction version. (Contributed by Thierry Arnoux, 17-Aug-2018.) |
Theorem | fmptco 6396* | Composition of two functions expressed as ordered-pair class abstractions. If has the equation and the equation then has the equation . (Contributed by FL, 21-Jun-2012.) (Revised by Mario Carneiro, 24-Jul-2014.) |
Theorem | fmptcof 6397* | Version of fmptco 6396 where needn't be distinct from . (Contributed by NM, 27-Dec-2014.) |
Theorem | fmptcos 6398* | Composition of two functions expressed as mapping abstractions. (Contributed by NM, 22-May-2006.) (Revised by Mario Carneiro, 31-Aug-2015.) |
Theorem | cofmpt 6399* | Express composition of a maps-to function with another function in a maps-to notation. (Contributed by Thierry Arnoux, 29-Jun-2017.) |
Theorem | fcompt 6400* | Express composition of two functions as a maps-to applying both in sequence. (Contributed by Stefan O'Rear, 5-Oct-2014.) (Proof shortened by Mario Carneiro, 27-Dec-2014.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |