Home Intuitionistic Logic ExplorerTheorem List (p. 56 of 133) < Previous  Next > Browser slow? Try the Unicode version. Mirrors  >  Metamath Home Page  >  ILE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Intuitionistic Logic Explorer - 5501-5600   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theoremfvmptdf 5501* Alternate deduction version of fvmpt 5491, suitable for iteration. (Contributed by Mario Carneiro, 7-Jan-2017.)

Theoremfvmptdv 5502* Alternate deduction version of fvmpt 5491, suitable for iteration. (Contributed by Mario Carneiro, 7-Jan-2017.)

Theoremfvmptdv2 5503* Alternate deduction version of fvmpt 5491, suitable for iteration. (Contributed by Mario Carneiro, 7-Jan-2017.)

Theoremmpteqb 5504* Bidirectional equality theorem for a mapping abstraction. Equivalent to eqfnfv 5511. (Contributed by Mario Carneiro, 14-Nov-2014.)

Theoremfvmptt 5505* Closed theorem form of fvmpt 5491. (Contributed by Scott Fenton, 21-Feb-2013.) (Revised by Mario Carneiro, 11-Sep-2015.)

Theoremfvmptf 5506* Value of a function given by an ordered-pair class abstraction. This version of fvmptg 5490 uses bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 8-Nov-2005.) (Revised by Mario Carneiro, 15-Oct-2016.)

Theoremfvmptd3 5507* Deduction version of fvmpt 5491. (Contributed by Glauco Siliprandi, 23-Oct-2021.)

Theoremelfvmptrab1 5508* 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.)

Theoremelfvmptrab 5509* 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.)

Theoremfvopab6 5510* Value of a function given by ordered-pair class abstraction. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 11-Sep-2015.)

Theoremeqfnfv 5511* 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.)

Theoremeqfnfv2 5512* 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.)

Theoremeqfnfv3 5513* Derive equality of functions from equality of their values. (Contributed by Jeff Madsen, 2-Sep-2009.)

Theoremeqfnfvd 5514* Deduction for equality of functions. (Contributed by Mario Carneiro, 24-Jul-2014.)

Theoremeqfnfv2f 5515* 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 5511 uses bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 29-Jan-2004.)

Theoremeqfunfv 5516* Equality of functions is determined by their values. (Contributed by Scott Fenton, 19-Jun-2011.)

Theoremfvreseq 5517* Equality of restricted functions is determined by their values. (Contributed by NM, 3-Aug-1994.)

Theoremfndmdif 5518* Two ways to express the locus of differences between two functions. (Contributed by Stefan O'Rear, 17-Jan-2015.)

Theoremfndmdifcom 5519 The difference set between two functions is commutative. (Contributed by Stefan O'Rear, 17-Jan-2015.)

Theoremfndmin 5520* Two ways to express the locus of equality between two functions. (Contributed by Stefan O'Rear, 17-Jan-2015.)

Theoremfneqeql 5521 Two functions are equal iff their equalizer is the whole domain. (Contributed by Stefan O'Rear, 7-Mar-2015.)

Theoremfneqeql2 5522 Two functions are equal iff their equalizer contains the whole domain. (Contributed by Stefan O'Rear, 9-Mar-2015.)

Theoremfnreseql 5523 Two functions are equal on a subset iff their equalizer contains that subset. (Contributed by Stefan O'Rear, 7-Mar-2015.)

Theoremchfnrn 5524* 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.)

Theoremfunfvop 5525 Ordered pair with function value. Part of Theorem 4.3(i) of [Monk1] p. 41. (Contributed by NM, 14-Oct-1996.)

Theoremfunfvbrb 5526 Two ways to say that is in the domain of . (Contributed by Mario Carneiro, 1-May-2014.)

Theoremfvimacnvi 5527 A member of a preimage is a function value argument. (Contributed by NM, 4-May-2007.)

Theoremfvimacnv 5528 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 5196 could probably be strengthened to a biconditional." (Contributed by Raph Levien, 20-Nov-2006.)

Theoremfunimass3 5529 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 5528 would be the special case of being a singleton, but it works this way round too." (Contributed by Raph Levien, 20-Nov-2006.)

Theoremfunimass5 5530* A subclass of a preimage in terms of function values. (Contributed by NM, 15-May-2007.)

Theoremfunconstss 5531* Two ways of specifying that a function is constant on a subdomain. (Contributed by NM, 8-Mar-2007.)

Theoremelpreima 5532 Membership in the preimage of a set under a function. (Contributed by Jeff Madsen, 2-Sep-2009.)

Theoremfniniseg 5533 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.)

Theoremfncnvima2 5534* Inverse images under functions expressed as abstractions. (Contributed by Stefan O'Rear, 1-Feb-2015.)

Theoremfniniseg2 5535* Inverse point images under functions expressed as abstractions. (Contributed by Stefan O'Rear, 1-Feb-2015.)

Theoremfnniniseg2 5536* Support sets of functions expressed as abstractions. (Contributed by Stefan O'Rear, 1-Feb-2015.)

Theoremrexsupp 5537* Existential quantification restricted to a support. (Contributed by Stefan O'Rear, 23-Mar-2015.)

Theoremunpreima 5538 Preimage of a union. (Contributed by Jeff Madsen, 2-Sep-2009.)

Theoreminpreima 5539 Preimage of an intersection. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 14-Jun-2016.)

Theoremdifpreima 5540 Preimage of a difference. (Contributed by Mario Carneiro, 14-Jun-2016.)

Theoremrespreima 5541 The preimage of a restricted function. (Contributed by Jeff Madsen, 2-Sep-2009.)

Theoremfimacnv 5542 The preimage of the codomain of a mapping is the mapping's domain. (Contributed by FL, 25-Jan-2007.)

Theoremfnopfv 5543 Ordered pair with function value. Part of Theorem 4.3(i) of [Monk1] p. 41. (Contributed by NM, 30-Sep-2004.)

Theoremfvelrn 5544 A function's value belongs to its range. (Contributed by NM, 14-Oct-1996.)

Theoremfnfvelrn 5545 A function's value belongs to its range. (Contributed by NM, 15-Oct-1996.)

Theoremffvelrn 5546 A function's value belongs to its codomain. (Contributed by NM, 12-Aug-1999.)

Theoremffvelrni 5547 A function's value belongs to its codomain. (Contributed by NM, 6-Apr-2005.)

Theoremffvelrnda 5548 A function's value belongs to its codomain. (Contributed by Mario Carneiro, 29-Dec-2016.)

Theoremffvelrnd 5549 A function's value belongs to its codomain. (Contributed by Mario Carneiro, 29-Dec-2016.)

Theoremrexrn 5550* Restricted existential quantification over the range of a function. (Contributed by Mario Carneiro, 24-Dec-2013.) (Revised by Mario Carneiro, 20-Aug-2014.)

Theoremralrn 5551* Restricted universal quantification over the range of a function. (Contributed by Mario Carneiro, 24-Dec-2013.) (Revised by Mario Carneiro, 20-Aug-2014.)

Theoremelrnrexdm 5552* 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.)

Theoremelrnrexdmb 5553* 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.)

Theoremeldmrexrn 5554* 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.)

Theoremralrnmpt 5555* A restricted quantifier over an image set. (Contributed by Mario Carneiro, 20-Aug-2015.)

Theoremrexrnmpt 5556* A restricted quantifier over an image set. (Contributed by Mario Carneiro, 20-Aug-2015.)

Theoremdff2 5557 Alternate definition of a mapping. (Contributed by NM, 14-Nov-2007.)

Theoremdff3im 5558* Property of a mapping. (Contributed by Jim Kingdon, 4-Jan-2019.)

Theoremdff4im 5559* Property of a mapping. (Contributed by Jim Kingdon, 4-Jan-2019.)

Theoremdffo3 5560* An onto mapping expressed in terms of function values. (Contributed by NM, 29-Oct-2006.)

Theoremdffo4 5561* Alternate definition of an onto mapping. (Contributed by NM, 20-Mar-2007.)

Theoremdffo5 5562* Alternate definition of an onto mapping. (Contributed by NM, 20-Mar-2007.)

Theoremfmpt 5563* Functionality of the mapping operation. (Contributed by Mario Carneiro, 26-Jul-2013.) (Revised by Mario Carneiro, 31-Aug-2015.)

Theoremf1ompt 5564* Express bijection for a mapping operation. (Contributed by Mario Carneiro, 30-May-2015.) (Revised by Mario Carneiro, 4-Dec-2016.)

Theoremfmpti 5565* Functionality of the mapping operation. (Contributed by NM, 19-Mar-2005.) (Revised by Mario Carneiro, 1-Sep-2015.)

Theoremfvmptelrn 5566* The value of a function at a point of its domain belongs to its codomain. (Contributed by Glauco Siliprandi, 26-Jun-2021.)

Theoremfmptd 5567* Domain and codomain of the mapping operation; deduction form. (Contributed by Mario Carneiro, 13-Jan-2013.)

Theoremfmpttd 5568* Version of fmptd 5567 with inlined definition. Domain and codomain of the mapping operation; deduction form. (Contributed by Glauco Siliprandi, 23-Oct-2021.) (Proof shortened by BJ, 16-Aug-2022.)

Theoremfmpt3d 5569* Domain and codomain of the mapping operation; deduction form. (Contributed by Thierry Arnoux, 4-Jun-2017.)

Theoremfmptdf 5570* A version of fmptd 5567 using bound-variable hypothesis instead of a distinct variable condition for . (Contributed by Glauco Siliprandi, 29-Jun-2017.)

Theoremffnfv 5571* A function maps to a class to which all values belong. (Contributed by NM, 3-Dec-2003.)

Theoremffnfvf 5572 A function maps to a class to which all values belong. This version of ffnfv 5571 uses bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 28-Sep-2006.)

Theoremfnfvrnss 5573* An upper bound for range determined by function values. (Contributed by NM, 8-Oct-2004.)

Theoremrnmptss 5574* The range of an operation given by the maps-to notation as a subset. (Contributed by Thierry Arnoux, 24-Sep-2017.)

Theoremfmpt2d 5575* Domain and codomain of the mapping operation; deduction form. (Contributed by NM, 27-Dec-2014.)

Theoremffvresb 5576* A necessary and sufficient condition for a restricted function. (Contributed by Mario Carneiro, 14-Nov-2013.)

Theoremresflem 5577* A lemma to bound the range of a restriction. The conclusion would also hold with in place of (provided does not occur in ). If that stronger result is needed, it is however simpler to use the instance of resflem 5577 where is substituted for (in both the conclusion and the third hypothesis). (Contributed by BJ, 4-Jul-2022.)

Theoremf1oresrab 5578* Build a bijection between restricted abstract builders, given a bijection between the base classes, deduction version. (Contributed by Thierry Arnoux, 17-Aug-2018.)

Theoremfmptco 5579* Composition of two functions expressed as ordered-pair class abstractions. If has the equation ( x + 2 ) and the equation ( 3 * z ) then has the equation ( 3 * ( x + 2 ) ) . (Contributed by FL, 21-Jun-2012.) (Revised by Mario Carneiro, 24-Jul-2014.)

Theoremfmptcof 5580* Version of fmptco 5579 where needn't be distinct from . (Contributed by NM, 27-Dec-2014.)

Theoremfmptcos 5581* Composition of two functions expressed as mapping abstractions. (Contributed by NM, 22-May-2006.) (Revised by Mario Carneiro, 31-Aug-2015.)

Theoremcofmpt 5582* Express composition of a maps-to function with another function in a maps-to notation. (Contributed by Thierry Arnoux, 29-Jun-2017.)

Theoremfcompt 5583* 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.)

Theoremfcoconst 5584 Composition with a constant function. (Contributed by Stefan O'Rear, 11-Mar-2015.)

Theoremfsn 5585 A function maps a singleton to a singleton iff it is the singleton of an ordered pair. (Contributed by NM, 10-Dec-2003.)

Theoremfsng 5586 A function maps a singleton to a singleton iff it is the singleton of an ordered pair. (Contributed by NM, 26-Oct-2012.)

Theoremfsn2 5587 A function that maps a singleton to a class is the singleton of an ordered pair. (Contributed by NM, 19-May-2004.)

Theoremxpsng 5588 The cross product of two singletons. (Contributed by Mario Carneiro, 30-Apr-2015.)

Theoremxpsn 5589 The cross product of two singletons. (Contributed by NM, 4-Nov-2006.)

Theoremdfmpt 5590 Alternate definition for the maps-to notation df-mpt 3986 (although it requires that be a set). (Contributed by NM, 24-Aug-2010.) (Revised by Mario Carneiro, 30-Dec-2016.)

Theoremfnasrn 5591 A function expressed as the range of another function. (Contributed by Mario Carneiro, 22-Jun-2013.) (Proof shortened by Mario Carneiro, 31-Aug-2015.)

Theoremdfmptg 5592 Alternate definition for the maps-to notation df-mpt 3986 (which requires that be a set). (Contributed by Jim Kingdon, 9-Jan-2019.)

Theoremfnasrng 5593 A function expressed as the range of another function. (Contributed by Jim Kingdon, 9-Jan-2019.)

Theoremressnop0 5594 If is not in , then the restriction of a singleton of to is null. (Contributed by Scott Fenton, 15-Apr-2011.)

Theoremfpr 5595 A function with a domain of two elements. (Contributed by Jeff Madsen, 20-Jun-2010.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)

Theoremfprg 5596 A function with a domain of two elements. (Contributed by FL, 2-Feb-2014.)

Theoremftpg 5597 A function with a domain of three elements. (Contributed by Alexander van der Vekens, 4-Dec-2017.)

Theoremftp 5598 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.)

Theoremfnressn 5599 A function restricted to a singleton. (Contributed by NM, 9-Oct-2004.)

Theoremfressnfv 5600 The value of a function restricted to a singleton. (Contributed by NM, 9-Oct-2004.)

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10600 107 10601-10700 108 10701-10800 109 10801-10900 110 10901-11000 111 11001-11100 112 11101-11200 113 11201-11300 114 11301-11400 115 11401-11500 116 11501-11600 117 11601-11700 118 11701-11800 119 11801-11900 120 11901-12000 121 12001-12100 122 12101-12200 123 12201-12300 124 12301-12400 125 12401-12500 126 12501-12600 127 12601-12700 128 12701-12800 129 12801-12900 130 12901-13000 131 13001-13100 132 13101-13200 133 13201-13235
 Copyright terms: Public domain < Previous  Next >