HomeHome Intuitionistic Logic Explorer
Theorem List (p. 56 of 94)
< 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
 
Theoremoprabbidv 5501* Equivalent wff's yield equal operation class abstractions (deduction rule). (Contributed by NM, 21-Feb-2004.)
   =>     { <.
 <. ,  >. ,  >.  |  }  { <. <. ,  >. ,  >.  |  }
 
Theoremoprabbii 5502* Equivalent wff's yield equal operation class abstractions. (Contributed by NM, 28-May-1995.) (Revised by David Abernethy, 19-Jun-2012.)
   =>     { <. <. ,  >. ,  >.  |  }  {
 <. <. ,  >. ,  >.  |  }
 
Theoremssoprab2 5503 Equivalence of ordered pair abstraction subclass and implication. Compare ssopab2 4003. (Contributed by FL, 6-Nov-2013.) (Proof shortened by Mario Carneiro, 11-Dec-2016.)
 { <.
 <. ,  >. ,  >.  |  }  C_  {
 <. <. ,  >. ,  >.  |  }
 
Theoremssoprab2b 5504 Equivalence of ordered pair abstraction subclass and implication. Compare ssopab2b 4004. (Contributed by FL, 6-Nov-2013.) (Proof shortened by Mario Carneiro, 11-Dec-2016.)
 { <. <. ,  >. ,  >.  |  }  C_  { <. <. ,  >. ,  >.  |  }
 
Theoremeqoprab2b 5505 Equivalence of ordered pair abstraction subclass and biconditional. Compare eqopab2b 4007. (Contributed by Mario Carneiro, 4-Jan-2017.)
 { <. <. ,  >. ,  >.  |  }  { <. <. ,  >. ,  >.  |  }
 
Theoremmpt2eq123 5506* An equality theorem for the maps to notation. (Contributed by Mario Carneiro, 16-Dec-2013.) (Revised by Mario Carneiro, 19-Mar-2015.)
 D  E  C  F  ,  |->  C  D ,  E  |->  F
 
Theoremmpt2eq12 5507* An equality theorem for the maps to notation. (Contributed by Mario Carneiro, 16-Dec-2013.)
 C  D  ,  |->  E  C ,  D  |->  E
 
Theoremmpt2eq123dva 5508* An equality deduction for the maps to notation. (Contributed by Mario Carneiro, 26-Jan-2017.)
 D   &     E   &    
 C  F   =>     ,  |->  C  D ,  E  |->  F
 
Theoremmpt2eq123dv 5509* An equality deduction for the maps to notation. (Contributed by NM, 12-Sep-2011.)
 D   &     E   &     C  F   =>     ,  |->  C  D ,  E  |->  F
 
Theoremmpt2eq123i 5510 An equality inference for the maps to notation. (Contributed by NM, 15-Jul-2013.)
 D   &     E   &     C  F   =>     ,  |->  C  D ,  E  |->  F
 
Theoremmpt2eq3dva 5511* Slightly more general equality inference for the maps to notation. (Contributed by NM, 17-Oct-2013.)
 C  D   =>     ,  |->  C  ,  |->  D
 
Theoremmpt2eq3ia 5512 An equality inference for the maps to notation. (Contributed by Mario Carneiro, 16-Dec-2013.)
 C  D   =>     ,  |->  C  ,  |->  D
 
Theoremnfmpt21 5513 Bound-variable hypothesis builder for an operation in maps-to notation. (Contributed by NM, 27-Aug-2013.)
 F/_  ,  |->  C
 
Theoremnfmpt22 5514 Bound-variable hypothesis builder for an operation in maps-to notation. (Contributed by NM, 27-Aug-2013.)
 F/_  ,  |->  C
 
Theoremnfmpt2 5515* Bound-variable hypothesis builder for the maps-to notation. (Contributed by NM, 20-Feb-2013.)
 F/_   &     F/_   &     F/_ C   =>     F/_  ,  |->  C
 
Theoremmpt20 5516 A mapping operation with empty domain. (Contributed by Stefan O'Rear, 29-Jan-2015.) (Revised by Mario Carneiro, 15-May-2015.)
 (/) ,  |->  C  (/)
 
Theoremoprab4 5517* Two ways to state the domain of an operation. (Contributed by FL, 24-Jan-2010.)

 { <. <. ,  >. ,  >.  | 
 <. ,  >.  X.  }  { <. <. ,  >. ,  >.  |  }
 
Theoremcbvoprab1 5518* 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.)

 F/   &     F/   &       =>     { <. <. ,  >. ,  >.  |  }  { <. <. ,  >. ,  >.  |  }
 
Theoremcbvoprab2 5519* Change the second bound variable in an operation abstraction. (Contributed by Jeff Madsen, 11-Jun-2010.) (Revised by Mario Carneiro, 11-Dec-2016.)

 F/   &     F/   &       =>     { <. <. ,  >. ,  >.  |  }  { <. <. ,  >. ,  >.  |  }
 
Theoremcbvoprab12 5520* 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.)

 F/   &     F/   &     F/   &     F/   &       =>    
 { <. <. ,  >. ,  >.  |  }  { <. <. ,  >. ,  >.  |  }
 
Theoremcbvoprab12v 5521* Rule used to change first two bound variables in an operation abstraction, using implicit substitution. (Contributed by NM, 8-Oct-2004.)
   =>    
 { <. <. ,  >. ,  >.  |  }  { <. <. ,  >. ,  >.  |  }
 
Theoremcbvoprab3 5522* Rule used to change the third bound variable in an operation abstraction, using implicit substitution. (Contributed by NM, 22-Aug-2013.)

 F/   &     F/   &       =>     { <. <. ,  >. ,  >.  |  }  { <. <. ,  >. ,  >.  |  }
 
Theoremcbvoprab3v 5523* 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 5524* Rule to change the bound variable in a maps-to function, using implicit substitution. This version of cbvmpt2 5525 allows to be a function of . (Contributed by NM, 29-Dec-2014.)
 F/_   &     F/_ D   &     F/_ C   &     F/_ C   &     F/_ E   &     F/_ E   &     D   &     C  E   =>     ,  |->  C  ,  D  |->  E
 
Theoremcbvmpt2 5525* Rule to change the bound variable in a maps-to function, using implicit substitution. (Contributed by NM, 17-Dec-2013.)
 F/_ C   &     F/_ C   &     F/_ D   &     F/_ D   &     C  D   =>     ,  |->  C  ,  |->  D
 
Theoremcbvmpt2v 5526* Rule to change the bound variable in a maps-to function, using implicit substitution. With a longer proof analogous to cbvmpt 3842, some distinct variable requirements could be eliminated. (Contributed by NM, 11-Jun-2013.)
 C  E   &     E  D   =>     ,  |->  C  ,  |->  D
 
Theoremdmoprab 5527* The domain of an operation class abstraction. (Contributed by NM, 17-Mar-1995.) (Revised by David Abernethy, 19-Jun-2012.)

 dom  { <. <. ,  >. ,  >.  |  }  { <. ,  >.  | 
 }
 
Theoremdmoprabss 5528* The domain of an operation class abstraction. (Contributed by NM, 24-Aug-1995.)

 dom  { <. <. ,  >. ,  >.  |  }  C_  X.
 
Theoremrnoprab 5529* The range of an operation class abstraction. (Contributed by NM, 30-Aug-2004.) (Revised by David Abernethy, 19-Apr-2013.)

 ran  { <. <. ,  >. ,  >.  |  }  {  |  }
 
Theoremrnoprab2 5530* The range of a restricted operation class abstraction. (Contributed by Scott Fenton, 21-Mar-2012.)

 ran  { <. <. ,  >. ,  >.  |  }  {  |  }
 
Theoremreldmoprab 5531* The domain of an operation class abstraction is a relation. (Contributed by NM, 17-Mar-1995.)

 Rel  dom  { <. <. ,  >. ,  >.  |  }
 
Theoremoprabss 5532* Structure of an operation class abstraction. (Contributed by NM, 28-Nov-2006.)

 { <. <. ,  >. ,  >.  |  } 
 C_  _V  X. 
 _V  X.  _V
 
Theoremeloprabga 5533* The law of concretion for operation class abstraction. Compare elopab 3986. (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.)
 C    =>     V  W  C  X  <. <. ,  >. ,  C >.  { <.
 <. ,  >. ,  >.  |  }
 
Theoremeloprabg 5534* The law of concretion for operation class abstraction. Compare elopab 3986. (Contributed by NM, 14-Sep-1999.) (Revised by David Abernethy, 19-Jun-2012.)
   &       &     C    =>     V  W  C  X  <. <. ,  >. ,  C >.  { <.
 <. ,  >. ,  >.  |  }
 
Theoremssoprab2i 5535* Inference of operation class abstraction subclass from implication. (Contributed by NM, 11-Nov-1995.) (Revised by David Abernethy, 19-Jun-2012.)
   =>    
 { <. <. ,  >. ,  >.  |  } 
 C_  { <. <. ,  >. ,  >.  |  }
 
Theoremmpt2v 5536* Operation with universal domain in maps-to notation. (Contributed by NM, 16-Aug-2013.)
 _V ,  _V  |->  C  { <. <. ,  >. ,  >.  |  C }
 
Theoremmpt2mptx 5537* 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.)
 <. ,  >.  C  D   =>     U_  { }  X. 
 |->  C  ,  |->  D
 
Theoremmpt2mpt 5538* 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.)
 <. ,  >.  C  D   =>     X.  |->  C  ,  |->  D
 
Theoremresoprab 5539* Restriction of an operation class abstraction. (Contributed by NM, 10-Feb-2007.)
 { <. <. ,  >. ,  >.  |  }  |`  X. 
 { <. <. ,  >. ,  >.  |  }
 
Theoremresoprab2 5540* Restriction of an operator abstraction. (Contributed by Jeff Madsen, 2-Sep-2009.)
 C  C_  D  C_  { <. <. ,  >. ,  >.  |  }  |`  C  X.  D  { <. <. ,  >. ,  >.  |  C  D  }
 
Theoremresmpt2 5541* Restriction of the mapping operation. (Contributed by Mario Carneiro, 17-Dec-2013.)
 C  C_  D  C_  ,  |->  E  |`  C  X.  D  C ,  D  |->  E
 
Theoremfunoprabg 5542* "At most one" is a sufficient condition for an operation class abstraction to be a function. (Contributed by NM, 28-Aug-2007.)
 Fun  { <. <. ,  >. ,  >.  |  }
 
Theoremfunoprab 5543* "At most one" is a sufficient condition for an operation class abstraction to be a function. (Contributed by NM, 17-Mar-1995.)
   =>    
 Fun  { <. <. ,  >. ,  >.  |  }
 
Theoremfnoprabg 5544* Functionality and domain of an operation class abstraction. (Contributed by NM, 28-Aug-2007.)
 { <.
 <. ,  >. ,  >.  |  }  Fn  {
 <. ,  >.  |  }
 
Theoremmpt2fun 5545* The maps-to notation for an operation is always a function. (Contributed by Scott Fenton, 21-Mar-2012.)
 F  ,  |->  C   =>     Fun  F
 
Theoremfnoprab 5546* Functionality and domain of an operation class abstraction. (Contributed by NM, 15-May-1995.)
   =>    
 { <. <. ,  >. ,  >.  |  }  Fn  { <. ,  >.  |  }
 
Theoremffnov 5547* An operation maps to a class to which all values belong. (Contributed by NM, 7-Feb-2004.)
 F :  X.  --> C  F  Fn  X.  F  C
 
Theoremfovcl 5548 Closure law for an operation. (Contributed by NM, 19-Apr-2007.)
 F : R  X.  S --> C   =>     R  S  F  C
 
Theoremeqfnov 5549* Equality of two operations is determined by their values. (Contributed by NM, 1-Sep-2005.)
 F  Fn  X.  G  Fn  C  X.  D  F  G  X.  C  X.  D  F  G
 
Theoremeqfnov2 5550* 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.)
 F  Fn  X.  G  Fn 
 X.  F  G  F  G
 
Theoremfnovim 5551* Representation of a function in terms of its values. (Contributed by Jim Kingdon, 16-Jan-2019.)
 F  Fn  X. 
 F  ,  |->  F
 
Theoremmpt22eqb 5552* Bidirectional equality theorem for a mapping abstraction. Equivalent to eqfnov2 5550. (Contributed by Mario Carneiro, 4-Jan-2017.)
 C  V  ,  |->  C  ,  |->  D  C  D
 
Theoremrnmpt2 5553* The range of an operation given by the "maps to" notation. (Contributed by FL, 20-Jun-2011.)
 F  ,  |->  C   =>     ran  F  {  |  C }
 
Theoremreldmmpt2 5554* The domain of an operation defined by maps-to notation is a relation. (Contributed by Stefan O'Rear, 27-Nov-2014.)
 F  ,  |->  C   =>     Rel  dom  F
 
Theoremelrnmpt2g 5555* Membership in the range of an operation class abstraction. (Contributed by NM, 27-Aug-2007.) (Revised by Mario Carneiro, 31-Aug-2015.)
 F  ,  |->  C   =>     D  V  D  ran  F  D  C
 
Theoremelrnmpt2 5556* Membership in the range of an operation class abstraction. (Contributed by NM, 1-Aug-2004.) (Revised by Mario Carneiro, 31-Aug-2015.)
 F  ,  |->  C   &     C  _V   =>     D  ran  F  D  C
 
Theoremralrnmpt2 5557* A restricted quantifier over an image set. (Contributed by Mario Carneiro, 1-Sep-2015.)
 F  ,  |->  C   &     C    =>     C  V  ran  F
 
Theoremrexrnmpt2 5558* A restricted quantifier over an image set. (Contributed by Mario Carneiro, 1-Sep-2015.)
 F  ,  |->  C   &     C    =>     C  V  ran  F
 
Theoremovid 5559* The value of an operation class abstraction. (Contributed by NM, 16-May-1995.) (Revised by David Abernethy, 19-Jun-2012.)
 R  S    &     F  { <. <. ,  >. ,  >.  |  R  S  }   =>     R  S  F
 
Theoremovidig 5560* The value of an operation class abstraction. Compare ovidi 5561. The condition  R  S is been removed. (Contributed by Mario Carneiro, 29-Dec-2014.)
   &     F  { <. <. ,  >. ,  >.  |  }   =>     F
 
Theoremovidi 5561* The value of an operation class abstraction (weak version). (Contributed by Mario Carneiro, 29-Dec-2014.)
 R  S    &     F  { <. <. ,  >. ,  >.  |  R  S  }   =>     R  S  F
 
Theoremov 5562* The value of an operation class abstraction. (Contributed by NM, 16-May-1995.) (Revised by David Abernethy, 19-Jun-2012.)
 C  _V   &       &       &     C    &     R  S    &     F  { <. <. ,  >. ,  >.  |  R  S  }   =>     R  S  F  C
 
Theoremovigg 5563* The value of an operation class abstraction. Compare ovig 5564. The condition  R  S is been removed. (Contributed by FL, 24-Mar-2007.) (Revised by Mario Carneiro, 19-Dec-2013.)
 C    &       &     F  { <. <. ,  >. ,  >.  |  }   =>     V  W  C  X  F  C
 
Theoremovig 5564* 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.)
 C    &     R  S    &     F  { <. <. ,  >. ,  >.  |  R  S  }   =>     R  S  C  D  F  C
 
Theoremovmpt4g 5565* Value of a function given by the "maps to" notation. (This is the operation analog of fvmpt2 5197.) (Contributed by NM, 21-Feb-2004.) (Revised by Mario Carneiro, 1-Sep-2015.)
 F  ,  |->  C   =>     C  V  F  C
 
Theoremovmpt2s 5566* Value of a function given by the "maps to" notation, expressed using explicit substitution. (Contributed by Mario Carneiro, 30-Apr-2015.)
 F  C ,  D  |->  R   =>     C  D  [_  ]_
 [_  ]_ R  V  F  [_  ]_ [_  ]_ R
 
Theoremov2gf 5567* The value of an operation class abstraction. A version of ovmpt2g 5577 using bound-variable hypotheses. (Contributed by NM, 17-Aug-2006.) (Revised by Mario Carneiro, 19-Dec-2013.)
 F/_   &     F/_   &     F/_   &     F/_ G   &     F/_ S   &     R  G   &     G  S   &     F  C ,  D  |->  R   =>     C  D  S  H  F  S
 
Theoremovmpt2dxf 5568* Value of an operation given by a maps-to rule, deduction form. (Contributed by Mario Carneiro, 29-Dec-2014.)
 F  C ,  D  |->  R   &    
 R  S   &     D  L   &     C   &     L   &     S  X   &     F/   &     F/   &     F/_   &     F/_   &     F/_ S   &     F/_ S   =>     F  S
 
Theoremovmpt2dx 5569* Value of an operation given by a maps-to rule, deduction form. (Contributed by Mario Carneiro, 29-Dec-2014.)
 F  C ,  D  |->  R   &    
 R  S   &     D  L   &     C   &     L   &     S  X   =>     F  S
 
Theoremovmpt2d 5570* Value of an operation given by a maps-to rule, deduction form. (Contributed by Mario Carneiro, 7-Dec-2014.)
 F  C ,  D  |->  R   &    
 R  S   &     C   &     D   &     S  X   =>     F  S
 
Theoremovmpt2x 5571* The value of an operation class abstraction. Variant of ovmpt2ga 5572 which does not require  D and to be distinct. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro, 20-Dec-2013.)
 R  S   &     D  L   &     F  C ,  D  |->  R   =>     C  L  S  H  F  S
 
Theoremovmpt2ga 5572* Value of an operation given by a maps-to rule. (Contributed by Mario Carneiro, 19-Dec-2013.)
 R  S   &     F  C ,  D  |->  R   =>     C  D  S  H  F  S
 
Theoremovmpt2a 5573* Value of an operation given by a maps-to rule. (Contributed by NM, 19-Dec-2013.)
 R  S   &     F  C ,  D  |->  R   &     S  _V   =>     C  D  F  S
 
Theoremovmpt2df 5574* Alternate deduction version of ovmpt2 5578, suitable for iteration. (Contributed by Mario Carneiro, 7-Jan-2017.)
 C   &     D   &    
 R  V   &     F  R    &     F/_ F   &     F/   &     F/_ F   &     F/   =>     F  C ,  D  |->  R
 
Theoremovmpt2dv 5575* Alternate deduction version of ovmpt2 5578, suitable for iteration. (Contributed by Mario Carneiro, 7-Jan-2017.)
 C   &     D   &    
 R  V   &     F  R    =>     F  C ,  D  |->  R
 
Theoremovmpt2dv2 5576* Alternate deduction version of ovmpt2 5578, suitable for iteration. (Contributed by Mario Carneiro, 7-Jan-2017.)
 C   &     D   &    
 R  V   &    
 R  S   =>     F  C ,  D  |->  R  F  S
 
Theoremovmpt2g 5577* 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.)
 R  G   &     G  S   &     F  C ,  D  |->  R   =>     C  D  S  H  F  S
 
Theoremovmpt2 5578* 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.)
 R  G   &     G  S   &     F  C ,  D  |->  R   &     S  _V   =>     C  D  F  S
 
Theoremovi3 5579* The value of an operation class abstraction. Special case. (Contributed by NM, 28-May-1995.) (Revised by Mario Carneiro, 29-Dec-2014.)
 H  H  C  H  D  H  S  H  X.  H   &     C  D  R  S   &     F  { <. <. ,  >. ,  >.  |  H  X.  H  H  X.  H  <. ,  >.  <. ,  >.  R }   =>     H  H  C  H  D  H  <. ,  >. F <. C ,  D >.  S
 
Theoremov6g 5580* The value of an operation class abstraction. Special case. (Contributed by NM, 13-Nov-2006.)
 <. ,  >.  <. ,  >.  R  S   &     F  { <. <. ,  >. ,  >.  |  <. ,  >.  C  R }   =>     G  H  <. ,  >.  C  S  J  F  S
 
Theoremovg 5581* The value of an operation class abstraction. (Contributed by Jeff Madsen, 10-Jun-2010.)
   &       &     C    &     R  S    &     F  { <. <. ,  >. ,  >.  |  R  S  }   =>     R  S  C  D  F  C
 
Theoremovres 5582 The value of a restricted operation. (Contributed by FL, 10-Nov-2006.)
 C  D  F  |`  C  X.  D  F
 
Theoremovresd 5583 Lemma for converting metric theorems to metric space theorems. (Contributed by Mario Carneiro, 2-Oct-2015.)
 X   &     X   =>     D  |`  X  X.  X  D
 
Theoremoprssov 5584 The value of a member of the domain of a subclass of an operation. (Contributed by NM, 23-Aug-2007.)
 Fun  F  G  Fn  C  X.  D  G  C_  F  C  D  F  G
 
Theoremfovrn 5585 An operation's value belongs to its codomain. (Contributed by NM, 27-Aug-2006.)
 F : R  X.  S --> C  R  S  F  C
 
Theoremfovrnda 5586 An operation's value belongs to its codomain. (Contributed by Mario Carneiro, 29-Dec-2016.)
 F : R  X.  S
 --> C   =>     R  S  F  C
 
Theoremfovrnd 5587 An operation's value belongs to its codomain. (Contributed by Mario Carneiro, 29-Dec-2016.)
 F : R  X.  S
 --> C   &     R   &     S   =>     F  C
 
Theoremfnrnov 5588* The range of an operation expressed as a collection of the operation's values. (Contributed by NM, 29-Oct-2006.)
 F  Fn  X.  ran  F  {  |  F }
 
Theoremfoov 5589* An onto mapping of an operation expressed in terms of operation values. (Contributed by NM, 29-Oct-2006.)
 F :  X. 
 -onto-> C  F :  X.  --> C  C  F
 
Theoremfnovrn 5590 An operation's value belongs to its range. (Contributed by NM, 10-Feb-2007.)
 F  Fn  X.  C  D  C F D  ran  F
 
Theoremovelrn 5591* 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.)
 F  Fn  X.  C  ran  F  C  F
 
Theoremfunimassov 5592* Membership relation for the values of a function whose image is a subclass. (Contributed by Mario Carneiro, 23-Dec-2013.)
 Fun  F  X.  C_  dom  F  F "  X.  C_  C  F  C
 
Theoremovelimab 5593* Operation value in an image. (Contributed by Mario Carneiro, 23-Dec-2013.) (Revised by Mario Carneiro, 29-Jan-2014.)
 F  Fn  X.  C  C_  D  F "  X.  C  C  D  F
 
Theoremovconst2 5594 The value of a constant operation. (Contributed by NM, 5-Nov-2006.)
 C  _V   =>     R  S  R  X.  X.  { C } S  C
 
Theoremcaovclg 5595* Convert an operation closure law to class notation. (Contributed by Mario Carneiro, 26-May-2014.)
 C  D  F  E   =>     C  D  F  E
 
Theoremcaovcld 5596* Convert an operation closure law to class notation. (Contributed by Mario Carneiro, 30-Dec-2014.)
 C  D  F  E   &     C   &     D   =>     F  E
 
Theoremcaovcl 5597* Convert an operation closure law to class notation. (Contributed by NM, 4-Aug-1995.) (Revised by Mario Carneiro, 26-May-2014.)
 S  S  F  S   =>     S  S  F  S
 
Theoremcaovcomg 5598* Convert an operation commutative law to class notation. (Contributed by Mario Carneiro, 1-Jun-2013.)
 S  S  F  F   =>     S  S  F  F
 
Theoremcaovcomd 5599* Convert an operation commutative law to class notation. (Contributed by Mario Carneiro, 30-Dec-2014.)
 S  S  F  F   &     S   &     S   =>     F  F
 
Theoremcaovcom 5600* Convert an operation commutative law to class notation. (Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 1-Jun-2013.)
 _V   &     _V   &     F  F   =>     F  F
    < Previous  Next >

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