Home Intuitionistic Logic ExplorerTheorem List (p. 57 of 106) < 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 - 5601-5700   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theoremnfmpt2 5601* Bound-variable hypothesis builder for the maps-to notation. (Contributed by NM, 20-Feb-2013.)

Theoremmpt20 5602 A mapping operation with empty domain. (Contributed by Stefan O'Rear, 29-Jan-2015.) (Revised by Mario Carneiro, 15-May-2015.)

Theoremoprab4 5603* Two ways to state the domain of an operation. (Contributed by FL, 24-Jan-2010.)

Theoremcbvoprab1 5604* Rule used to change first bound variable in an operation abstraction, using implicit substitution. (Contributed by NM, 20-Dec-2008.) (Revised by Mario Carneiro, 5-Dec-2016.)

Theoremcbvoprab2 5605* Change the second bound variable in an operation abstraction. (Contributed by Jeff Madsen, 11-Jun-2010.) (Revised by Mario Carneiro, 11-Dec-2016.)

Theoremcbvoprab12 5606* Rule used to change first two bound variables in an operation abstraction, using implicit substitution. (Contributed by NM, 21-Feb-2004.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)

Theoremcbvoprab12v 5607* Rule used to change first two bound variables in an operation abstraction, using implicit substitution. (Contributed by NM, 8-Oct-2004.)

Theoremcbvoprab3 5608* Rule used to change the third bound variable in an operation abstraction, using implicit substitution. (Contributed by NM, 22-Aug-2013.)

Theoremcbvoprab3v 5609* Rule used to change the third bound variable in an operation abstraction, using implicit substitution. (Contributed by NM, 8-Oct-2004.) (Revised by David Abernethy, 19-Jun-2012.)

Theoremcbvmpt2x 5610* Rule to change the bound variable in a maps-to function, using implicit substitution. This version of cbvmpt2 5611 allows to be a function of . (Contributed by NM, 29-Dec-2014.)

Theoremcbvmpt2 5611* Rule to change the bound variable in a maps-to function, using implicit substitution. (Contributed by NM, 17-Dec-2013.)

Theoremcbvmpt2v 5612* Rule to change the bound variable in a maps-to function, using implicit substitution. With a longer proof analogous to cbvmpt 3879, some distinct variable requirements could be eliminated. (Contributed by NM, 11-Jun-2013.)

Theoremdmoprab 5613* The domain of an operation class abstraction. (Contributed by NM, 17-Mar-1995.) (Revised by David Abernethy, 19-Jun-2012.)

Theoremdmoprabss 5614* The domain of an operation class abstraction. (Contributed by NM, 24-Aug-1995.)

Theoremrnoprab 5615* The range of an operation class abstraction. (Contributed by NM, 30-Aug-2004.) (Revised by David Abernethy, 19-Apr-2013.)

Theoremrnoprab2 5616* The range of a restricted operation class abstraction. (Contributed by Scott Fenton, 21-Mar-2012.)

Theoremreldmoprab 5617* The domain of an operation class abstraction is a relation. (Contributed by NM, 17-Mar-1995.)

Theoremoprabss 5618* Structure of an operation class abstraction. (Contributed by NM, 28-Nov-2006.)

Theoremeloprabga 5619* The law of concretion for operation class abstraction. Compare elopab 4023. (Contributed by NM, 14-Sep-1999.) (Unnecessary distinct variable restrictions were removed by David Abernethy, 19-Jun-2012.) (Revised by Mario Carneiro, 19-Dec-2013.)

Theoremeloprabg 5620* The law of concretion for operation class abstraction. Compare elopab 4023. (Contributed by NM, 14-Sep-1999.) (Revised by David Abernethy, 19-Jun-2012.)

Theoremssoprab2i 5621* Inference of operation class abstraction subclass from implication. (Contributed by NM, 11-Nov-1995.) (Revised by David Abernethy, 19-Jun-2012.)

Theoremmpt2v 5622* Operation with universal domain in maps-to notation. (Contributed by NM, 16-Aug-2013.)

Theoremmpt2mptx 5623* Express a two-argument function as a one-argument function, or vice-versa. In this version is not assumed to be constant w.r.t . (Contributed by Mario Carneiro, 29-Dec-2014.)

Theoremmpt2mpt 5624* Express a two-argument function as a one-argument function, or vice-versa. (Contributed by Mario Carneiro, 17-Dec-2013.) (Revised by Mario Carneiro, 29-Dec-2014.)

Theoremresoprab 5625* Restriction of an operation class abstraction. (Contributed by NM, 10-Feb-2007.)

Theoremresoprab2 5626* Restriction of an operator abstraction. (Contributed by Jeff Madsen, 2-Sep-2009.)

Theoremresmpt2 5627* Restriction of the mapping operation. (Contributed by Mario Carneiro, 17-Dec-2013.)

Theoremfunoprabg 5628* "At most one" is a sufficient condition for an operation class abstraction to be a function. (Contributed by NM, 28-Aug-2007.)

Theoremfunoprab 5629* "At most one" is a sufficient condition for an operation class abstraction to be a function. (Contributed by NM, 17-Mar-1995.)

Theoremfnoprabg 5630* Functionality and domain of an operation class abstraction. (Contributed by NM, 28-Aug-2007.)

Theoremmpt2fun 5631* The maps-to notation for an operation is always a function. (Contributed by Scott Fenton, 21-Mar-2012.)

Theoremfnoprab 5632* Functionality and domain of an operation class abstraction. (Contributed by NM, 15-May-1995.)

Theoremffnov 5633* An operation maps to a class to which all values belong. (Contributed by NM, 7-Feb-2004.)

Theoremfovcl 5634 Closure law for an operation. (Contributed by NM, 19-Apr-2007.)

Theoremeqfnov 5635* Equality of two operations is determined by their values. (Contributed by NM, 1-Sep-2005.)

Theoremeqfnov2 5636* Two operators with the same domain are equal iff their values at each point in the domain are equal. (Contributed by Jeff Madsen, 7-Jun-2010.)

Theoremfnovim 5637* Representation of a function in terms of its values. (Contributed by Jim Kingdon, 16-Jan-2019.)

Theoremmpt22eqb 5638* Bidirectional equality theorem for a mapping abstraction. Equivalent to eqfnov2 5636. (Contributed by Mario Carneiro, 4-Jan-2017.)

Theoremrnmpt2 5639* The range of an operation given by the "maps to" notation. (Contributed by FL, 20-Jun-2011.)

Theoremreldmmpt2 5640* The domain of an operation defined by maps-to notation is a relation. (Contributed by Stefan O'Rear, 27-Nov-2014.)

Theoremelrnmpt2g 5641* Membership in the range of an operation class abstraction. (Contributed by NM, 27-Aug-2007.) (Revised by Mario Carneiro, 31-Aug-2015.)

Theoremelrnmpt2 5642* Membership in the range of an operation class abstraction. (Contributed by NM, 1-Aug-2004.) (Revised by Mario Carneiro, 31-Aug-2015.)

Theoremralrnmpt2 5643* A restricted quantifier over an image set. (Contributed by Mario Carneiro, 1-Sep-2015.)

Theoremrexrnmpt2 5644* A restricted quantifier over an image set. (Contributed by Mario Carneiro, 1-Sep-2015.)

Theoremovid 5645* The value of an operation class abstraction. (Contributed by NM, 16-May-1995.) (Revised by David Abernethy, 19-Jun-2012.)

Theoremovidig 5646* The value of an operation class abstraction. Compare ovidi 5647. The condition is been removed. (Contributed by Mario Carneiro, 29-Dec-2014.)

Theoremovidi 5647* The value of an operation class abstraction (weak version). (Contributed by Mario Carneiro, 29-Dec-2014.)

Theoremov 5648* The value of an operation class abstraction. (Contributed by NM, 16-May-1995.) (Revised by David Abernethy, 19-Jun-2012.)

Theoremovigg 5649* The value of an operation class abstraction. Compare ovig 5650. The condition is been removed. (Contributed by FL, 24-Mar-2007.) (Revised by Mario Carneiro, 19-Dec-2013.)

Theoremovig 5650* The value of an operation class abstraction (weak version). (Unnecessary distinct variable restrictions were removed by David Abernethy, 19-Jun-2012.) (Contributed by NM, 14-Sep-1999.) (Revised by Mario Carneiro, 19-Dec-2013.)

Theoremovmpt4g 5651* Value of a function given by the "maps to" notation. (This is the operation analog of fvmpt2 5282.) (Contributed by NM, 21-Feb-2004.) (Revised by Mario Carneiro, 1-Sep-2015.)

Theoremovmpt2s 5652* Value of a function given by the "maps to" notation, expressed using explicit substitution. (Contributed by Mario Carneiro, 30-Apr-2015.)

Theoremov2gf 5653* The value of an operation class abstraction. A version of ovmpt2g 5663 using bound-variable hypotheses. (Contributed by NM, 17-Aug-2006.) (Revised by Mario Carneiro, 19-Dec-2013.)

Theoremovmpt2dxf 5654* Value of an operation given by a maps-to rule, deduction form. (Contributed by Mario Carneiro, 29-Dec-2014.)

Theoremovmpt2dx 5655* Value of an operation given by a maps-to rule, deduction form. (Contributed by Mario Carneiro, 29-Dec-2014.)

Theoremovmpt2d 5656* Value of an operation given by a maps-to rule, deduction form. (Contributed by Mario Carneiro, 7-Dec-2014.)

Theoremovmpt2x 5657* The value of an operation class abstraction. Variant of ovmpt2ga 5658 which does not require and to be distinct. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro, 20-Dec-2013.)

Theoremovmpt2ga 5658* Value of an operation given by a maps-to rule. (Contributed by Mario Carneiro, 19-Dec-2013.)

Theoremovmpt2a 5659* Value of an operation given by a maps-to rule. (Contributed by NM, 19-Dec-2013.)

Theoremovmpt2df 5660* Alternate deduction version of ovmpt2 5664, suitable for iteration. (Contributed by Mario Carneiro, 7-Jan-2017.)

Theoremovmpt2dv 5661* Alternate deduction version of ovmpt2 5664, suitable for iteration. (Contributed by Mario Carneiro, 7-Jan-2017.)

Theoremovmpt2dv2 5662* Alternate deduction version of ovmpt2 5664, suitable for iteration. (Contributed by Mario Carneiro, 7-Jan-2017.)

Theoremovmpt2g 5663* Value of an operation given by a maps-to rule. Special case. (Contributed by NM, 14-Sep-1999.) (Revised by David Abernethy, 19-Jun-2012.)

Theoremovmpt2 5664* Value of an operation given by a maps-to rule. Special case. (Contributed by NM, 16-May-1995.) (Revised by David Abernethy, 19-Jun-2012.)

Theoremovi3 5665* The value of an operation class abstraction. Special case. (Contributed by NM, 28-May-1995.) (Revised by Mario Carneiro, 29-Dec-2014.)

Theoremov6g 5666* The value of an operation class abstraction. Special case. (Contributed by NM, 13-Nov-2006.)

Theoremovg 5667* The value of an operation class abstraction. (Contributed by Jeff Madsen, 10-Jun-2010.)

Theoremovres 5668 The value of a restricted operation. (Contributed by FL, 10-Nov-2006.)

Theoremovresd 5669 Lemma for converting metric theorems to metric space theorems. (Contributed by Mario Carneiro, 2-Oct-2015.)

Theoremoprssov 5670 The value of a member of the domain of a subclass of an operation. (Contributed by NM, 23-Aug-2007.)

Theoremfovrn 5671 An operation's value belongs to its codomain. (Contributed by NM, 27-Aug-2006.)

Theoremfovrnda 5672 An operation's value belongs to its codomain. (Contributed by Mario Carneiro, 29-Dec-2016.)

Theoremfovrnd 5673 An operation's value belongs to its codomain. (Contributed by Mario Carneiro, 29-Dec-2016.)

Theoremfnrnov 5674* The range of an operation expressed as a collection of the operation's values. (Contributed by NM, 29-Oct-2006.)

Theoremfoov 5675* An onto mapping of an operation expressed in terms of operation values. (Contributed by NM, 29-Oct-2006.)

Theoremfnovrn 5676 An operation's value belongs to its range. (Contributed by NM, 10-Feb-2007.)

Theoremovelrn 5677* A member of an operation's range is a value of the operation. (Contributed by NM, 7-Feb-2007.) (Revised by Mario Carneiro, 30-Jan-2014.)

Theoremfunimassov 5678* Membership relation for the values of a function whose image is a subclass. (Contributed by Mario Carneiro, 23-Dec-2013.)

Theoremovelimab 5679* Operation value in an image. (Contributed by Mario Carneiro, 23-Dec-2013.) (Revised by Mario Carneiro, 29-Jan-2014.)

Theoremovconst2 5680 The value of a constant operation. (Contributed by NM, 5-Nov-2006.)

Theoremcaovclg 5681* Convert an operation closure law to class notation. (Contributed by Mario Carneiro, 26-May-2014.)

Theoremcaovcld 5682* Convert an operation closure law to class notation. (Contributed by Mario Carneiro, 30-Dec-2014.)

Theoremcaovcl 5683* Convert an operation closure law to class notation. (Contributed by NM, 4-Aug-1995.) (Revised by Mario Carneiro, 26-May-2014.)

Theoremcaovcomg 5684* Convert an operation commutative law to class notation. (Contributed by Mario Carneiro, 1-Jun-2013.)

Theoremcaovcomd 5685* Convert an operation commutative law to class notation. (Contributed by Mario Carneiro, 30-Dec-2014.)

Theoremcaovcom 5686* Convert an operation commutative law to class notation. (Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 1-Jun-2013.)

Theoremcaovassg 5687* Convert an operation associative law to class notation. (Contributed by Mario Carneiro, 1-Jun-2013.) (Revised by Mario Carneiro, 26-May-2014.)

Theoremcaovassd 5688* Convert an operation associative law to class notation. (Contributed by Mario Carneiro, 30-Dec-2014.)

Theoremcaovass 5689* Convert an operation associative law to class notation. (Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 26-May-2014.)

Theoremcaovcang 5690* Convert an operation cancellation law to class notation. (Contributed by NM, 20-Aug-1995.) (Revised by Mario Carneiro, 30-Dec-2014.)

Theoremcaovcand 5691* Convert an operation cancellation law to class notation. (Contributed by Mario Carneiro, 30-Dec-2014.)

Theoremcaovcanrd 5692* Commute the arguments of an operation cancellation law. (Contributed by Mario Carneiro, 30-Dec-2014.)

Theoremcaovcan 5693* Convert an operation cancellation law to class notation. (Contributed by NM, 20-Aug-1995.)

Theoremcaovordig 5694* Convert an operation ordering law to class notation. (Contributed by Mario Carneiro, 31-Dec-2014.)

Theoremcaovordid 5695* Convert an operation ordering law to class notation. (Contributed by Mario Carneiro, 31-Dec-2014.)

Theoremcaovordg 5696* Convert an operation ordering law to class notation. (Contributed by NM, 19-Feb-1996.) (Revised by Mario Carneiro, 30-Dec-2014.)

Theoremcaovordd 5697* Convert an operation ordering law to class notation. (Contributed by Mario Carneiro, 30-Dec-2014.)

Theoremcaovord2d 5698* Operation ordering law with commuted arguments. (Contributed by Mario Carneiro, 30-Dec-2014.)

Theoremcaovord3d 5699* Ordering law. (Contributed by Mario Carneiro, 30-Dec-2014.)

Theoremcaovord 5700* Convert an operation ordering law to class notation. (Contributed by NM, 19-Feb-1996.)

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-10511
 Copyright terms: Public domain < Previous  Next >