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

Definition df-ov 5745
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 𝐹 and its arguments 𝐴 and 𝐵- will be useful for proving meaningful theorems. For example, if class 𝐹 is the operation + and arguments 𝐴 and 𝐵 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 𝐴 and/or 𝐵 are proper classes (i.e. are not sets); see ovprc1 5775 and ovprc2 5776. On the other hand, we often find uses for this definition when 𝐹 is a proper class. 𝐹 is normally equal to a class of nested ordered pairs of the form defined by df-oprab 5746. (Contributed by NM, 28-Feb-1995.)
Assertion
Ref Expression
df-ov (𝐴𝐹𝐵) = (𝐹‘⟨𝐴, 𝐵⟩)

Detailed syntax breakdown of Definition df-ov
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cB . . 3 class 𝐵
3 cF . . 3 class 𝐹
41, 2, 3co 5742 . 2 class (𝐴𝐹𝐵)
51, 2cop 3500 . . 3 class 𝐴, 𝐵
65, 3cfv 5093 . 2 class (𝐹‘⟨𝐴, 𝐵⟩)
74, 6wceq 1316 1 wff (𝐴𝐹𝐵) = (𝐹‘⟨𝐴, 𝐵⟩)
Colors of variables: wff set class
This definition is referenced by:  oveq  5748  oveq1  5749  oveq2  5750  nfovd  5768  fnovex  5772  ovexg  5773  ovprc  5774  fnotovb  5782  ffnov  5843  eqfnov  5845  fnovim  5847  ovid  5855  ovidig  5856  ov  5858  ovigg  5859  ov6g  5876  ovg  5877  ovres  5878  fovrn  5881  fnrnov  5884  foov  5885  fnovrn  5886  funimassov  5888  ovelimab  5889  ovconst2  5890  elmpocl  5936  oprssdmm  6037  mpofvex  6069  oprab2co  6083  algrflem  6094  algrflemg  6095  mpoxopn0yelv  6104  ovtposg  6124  addpiord  7092  mulpiord  7093  addvalex  7620  cnref1o  9396  ioof  9709  frecuzrdgrrn  10136  frec2uzrdg  10137  frecuzrdgrcl  10138  frecuzrdgsuc  10142  frecuzrdgrclt  10143  frecuzrdgg  10144  frecuzrdgsuctlem  10151  seq3val  10186  seqvalcd  10187  cnrecnv  10637  eucalgval  11647  eucalginv  11649  eucalglt  11650  eucalg  11652  sqpweven  11764  2sqpwodd  11765  isstructim  11884  isstructr  11885  txdis1cn  12358  lmcn2  12360  cnmpt12f  12366  cnmpt21  12371  cnmpt2t  12373  cnmpt22  12374  psmetxrge0  12412  xmeterval  12515  comet  12579  txmetcnp  12598  qtopbasss  12601  cnmetdval  12609  remetdval  12619  tgqioo  12627
  Copyright terms: Public domain W3C validator