Home Intuitionistic Logic ExplorerTheorem List (p. 57 of 102) < 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

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

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

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

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

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

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

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

Theoremeqfnov2 5608* 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 5609* Representation of a function in terms of its values. (Contributed by Jim Kingdon, 16-Jan-2019.)

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

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

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

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

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

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

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

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

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

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

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

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

Theoremovig 5622* 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 5623* Value of a function given by the "maps to" notation. (This is the operation analog of fvmpt2 5254.) (Contributed by NM, 21-Feb-2004.) (Revised by Mario Carneiro, 1-Sep-2015.)

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

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

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

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

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

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

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

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

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

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

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

Theoremovmpt2g 5635* 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 5636* 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 5637* The value of an operation class abstraction. Special case. (Contributed by NM, 28-May-1995.) (Revised by Mario Carneiro, 29-Dec-2014.)

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

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

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

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

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

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

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

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

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

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

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

Theoremovelrn 5649* 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 5650* Membership relation for the values of a function whose image is a subclass. (Contributed by Mario Carneiro, 23-Dec-2013.)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Theoremcaovord2 5673* Operation ordering law with commuted arguments. (Contributed by NM, 27-Feb-1996.)

Theoremcaovord3 5674* Ordering law. (Contributed by NM, 29-Feb-1996.)

Theoremcaovdig 5675* Convert an operation distributive law to class notation. (Contributed by NM, 25-Aug-1995.) (Revised by Mario Carneiro, 26-Jul-2014.)

Theoremcaovdid 5676* Convert an operation distributive law to class notation. (Contributed by Mario Carneiro, 30-Dec-2014.)

Theoremcaovdir2d 5677* Convert an operation distributive law to class notation. (Contributed by Mario Carneiro, 30-Dec-2014.)

Theoremcaovdirg 5678* Convert an operation reverse distributive law to class notation. (Contributed by Mario Carneiro, 19-Oct-2014.)

Theoremcaovdird 5679* Convert an operation distributive law to class notation. (Contributed by Mario Carneiro, 30-Dec-2014.)

Theoremcaovdi 5680* Convert an operation distributive law to class notation. (Contributed by NM, 25-Aug-1995.) (Revised by Mario Carneiro, 28-Jun-2013.)

Theoremcaov32d 5681* Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 30-Dec-2014.)

Theoremcaov12d 5682* Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 30-Dec-2014.)

Theoremcaov31d 5683* Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 30-Dec-2014.)

Theoremcaov13d 5684* Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 30-Dec-2014.)

Theoremcaov4d 5685* Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 30-Dec-2014.)

Theoremcaov411d 5686* Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 30-Dec-2014.)

Theoremcaov42d 5687* Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 30-Dec-2014.)

Theoremcaov32 5688* Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.)

Theoremcaov12 5689* Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.)

Theoremcaov31 5690* Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.)

Theoremcaov13 5691* Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.)

Theoremcaovdilemd 5692* Lemma used by real number construction. (Contributed by Jim Kingdon, 16-Sep-2019.)

Theoremcaovlem2d 5693* Rearrangement of expression involving multiplication () and addition (). (Contributed by Jim Kingdon, 3-Jan-2020.)

Theoremcaovimo 5694* Uniqueness of inverse element in commutative, associative operation with identity. The identity element is . (Contributed by Jim Kingdon, 18-Sep-2019.)

Theoremgrprinvlem 5695* Lemma for grprinvd 5696. (Contributed by NM, 9-Aug-2013.)

Theoremgrprinvd 5696* Deduce right inverse from left inverse and left identity in an associative structure (such as a group). (Contributed by NM, 10-Aug-2013.) (Proof shortened by Mario Carneiro, 6-Jan-2015.)

Theoremgrpridd 5697* Deduce right identity from left inverse and left identity in an associative structure (such as a group). (Contributed by NM, 10-Aug-2013.) (Proof shortened by Mario Carneiro, 6-Jan-2015.)

2.6.11  "Maps to" notation

Theoremelmpt2cl 5698* If a two-parameter class is not empty, constrain the implicit pair. (Contributed by Stefan O'Rear, 7-Mar-2015.)

Theoremelmpt2cl1 5699* If a two-parameter class is not empty, the first argument is in its nominal domain. (Contributed by FL, 15-Oct-2012.) (Revised by Stefan O'Rear, 7-Mar-2015.)

Theoremelmpt2cl2 5700* If a two-parameter class is not empty, the second argument is in its nominal domain. (Contributed by FL, 15-Oct-2012.) (Revised by Stefan O'Rear, 7-Mar-2015.)

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