ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-ov Unicode version

Definition df-ov 5542
Description: Define the value of an operation. Definition of operation value in [Enderton] p. 79. Note that the syntax is simply three class expressions in a row bracketed by parentheses. There are no restrictions of any kind on what those class expressions may be, although only certain kinds of class expressions - a binary operation  F and its arguments  A and  B- will be useful for proving meaningful theorems. For example, if class  F is the operation + and arguments  A and  B are 3 and 2 , the expression ( 3 + 2 ) can be proved to equal 5 . This definition is well-defined, although not very meaningful, when classes  A and/or  B are proper classes (i.e. are not sets); see ovprc1 5568 and ovprc2 5569. On the other hand, we often find uses for this definition when  F is a proper class.  F is normally equal to a class of nested ordered pairs of the form defined by df-oprab 5543. (Contributed by NM, 28-Feb-1995.)
Assertion
Ref Expression
df-ov  |-  ( A F B )  =  ( F `  <. A ,  B >. )

Detailed syntax breakdown of Definition df-ov
StepHypRef Expression
1 cA . . 3  class  A
2 cB . . 3  class  B
3 cF . . 3  class  F
41, 2, 3co 5539 . 2  class  ( A F B )
51, 2cop 3405 . . 3  class  <. A ,  B >.
65, 3cfv 4929 . 2  class  ( F `
 <. A ,  B >. )
74, 6wceq 1259 1  wff  ( A F B )  =  ( F `  <. A ,  B >. )
Colors of variables: wff set class
This definition is referenced by:  oveq  5545  oveq1  5546  oveq2  5547  nfovd  5561  fnovex  5565  ovexg  5566  ovprc  5567  fnotovb  5575  ffnov  5632  eqfnov  5634  fnovim  5636  ovid  5644  ovidig  5645  ov  5647  ovigg  5648  ov6g  5665  ovg  5666  ovres  5667  fovrn  5670  fnrnov  5673  foov  5674  fnovrn  5675  funimassov  5677  ovelimab  5678  ovconst2  5679  elmpt2cl  5725  mpt2fvex  5856  oprab2co  5866  algrflem  5877  algrflemg  5878  mpt2xopn0yelv  5884  ovtposg  5904  addpiord  6471  mulpiord  6472  addvalex  6977  cnref1o  8679  ioof  8940  frecuzrdgrrn  9357  frec2uzrdg  9358  frecuzrdgsuc  9364  cnrecnv  9737
  Copyright terms: Public domain W3C validator