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

Definition df-ov 5777
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 5807 and ovprc2 5808. 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 5778. (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 5774 . 2  class  ( A F B )
51, 2cop 3530 . . 3  class  <. A ,  B >.
65, 3cfv 5123 . 2  class  ( F `
 <. A ,  B >. )
74, 6wceq 1331 1  wff  ( A F B )  =  ( F `  <. A ,  B >. )
Colors of variables: wff set class
This definition is referenced by:  oveq  5780  oveq1  5781  oveq2  5782  nfovd  5800  fnovex  5804  ovexg  5805  ovprc  5806  fnotovb  5814  ffnov  5875  eqfnov  5877  fnovim  5879  ovid  5887  ovidig  5888  ov  5890  ovigg  5891  ov6g  5908  ovg  5909  ovres  5910  fovrn  5913  fnrnov  5916  foov  5917  fnovrn  5918  funimassov  5920  ovelimab  5921  ovconst2  5922  elmpocl  5968  oprssdmm  6069  mpofvex  6101  oprab2co  6115  algrflem  6126  algrflemg  6127  mpoxopn0yelv  6136  ovtposg  6156  addpiord  7136  mulpiord  7137  addvalex  7664  cnref1o  9452  ioof  9766  frecuzrdgrrn  10193  frec2uzrdg  10194  frecuzrdgrcl  10195  frecuzrdgsuc  10199  frecuzrdgrclt  10200  frecuzrdgg  10201  frecuzrdgsuctlem  10208  seq3val  10243  seqvalcd  10244  cnrecnv  10694  eucalgval  11746  eucalginv  11748  eucalglt  11749  eucalg  11751  sqpweven  11864  2sqpwodd  11865  isstructim  11987  isstructr  11988  txdis1cn  12461  lmcn2  12463  cnmpt12f  12469  cnmpt21  12474  cnmpt2t  12476  cnmpt22  12477  psmetxrge0  12515  xmeterval  12618  comet  12682  txmetcnp  12701  qtopbasss  12704  cnmetdval  12712  remetdval  12722  tgqioo  12730
  Copyright terms: Public domain W3C validator