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

Definition df-ov 5770
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 5800 and ovprc2 5801. 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 5771. (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 5767 . 2 class (𝐴𝐹𝐵)
51, 2cop 3525 . . 3 class 𝐴, 𝐵
65, 3cfv 5118 . 2 class (𝐹‘⟨𝐴, 𝐵⟩)
74, 6wceq 1331 1 wff (𝐴𝐹𝐵) = (𝐹‘⟨𝐴, 𝐵⟩)
Colors of variables: wff set class
This definition is referenced by:  oveq  5773  oveq1  5774  oveq2  5775  nfovd  5793  fnovex  5797  ovexg  5798  ovprc  5799  fnotovb  5807  ffnov  5868  eqfnov  5870  fnovim  5872  ovid  5880  ovidig  5881  ov  5883  ovigg  5884  ov6g  5901  ovg  5902  ovres  5903  fovrn  5906  fnrnov  5909  foov  5910  fnovrn  5911  funimassov  5913  ovelimab  5914  ovconst2  5915  elmpocl  5961  oprssdmm  6062  mpofvex  6094  oprab2co  6108  algrflem  6119  algrflemg  6120  mpoxopn0yelv  6129  ovtposg  6149  addpiord  7117  mulpiord  7118  addvalex  7645  cnref1o  9433  ioof  9747  frecuzrdgrrn  10174  frec2uzrdg  10175  frecuzrdgrcl  10176  frecuzrdgsuc  10180  frecuzrdgrclt  10181  frecuzrdgg  10182  frecuzrdgsuctlem  10189  seq3val  10224  seqvalcd  10225  cnrecnv  10675  eucalgval  11724  eucalginv  11726  eucalglt  11727  eucalg  11729  sqpweven  11842  2sqpwodd  11843  isstructim  11962  isstructr  11963  txdis1cn  12436  lmcn2  12438  cnmpt12f  12444  cnmpt21  12449  cnmpt2t  12451  cnmpt22  12452  psmetxrge0  12490  xmeterval  12593  comet  12657  txmetcnp  12676  qtopbasss  12679  cnmetdval  12687  remetdval  12697  tgqioo  12705
  Copyright terms: Public domain W3C validator