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

Definition df-ov 5543
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 5569 and ovprc2 5570. 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 5544. (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 5540 . 2 class (𝐴𝐹𝐵)
51, 2cop 3406 . . 3 class 𝐴, 𝐵
65, 3cfv 4930 . 2 class (𝐹‘⟨𝐴, 𝐵⟩)
74, 6wceq 1259 1 wff (𝐴𝐹𝐵) = (𝐹‘⟨𝐴, 𝐵⟩)
Colors of variables: wff set class
This definition is referenced by:  oveq  5546  oveq1  5547  oveq2  5548  nfovd  5562  fnovex  5566  ovexg  5567  ovprc  5568  fnotovb  5576  ffnov  5633  eqfnov  5635  fnovim  5637  ovid  5645  ovidig  5646  ov  5648  ovigg  5649  ov6g  5666  ovg  5667  ovres  5668  fovrn  5671  fnrnov  5674  foov  5675  fnovrn  5676  funimassov  5678  ovelimab  5679  ovconst2  5680  elmpt2cl  5726  mpt2fvex  5857  oprab2co  5867  algrflem  5878  algrflemg  5879  mpt2xopn0yelv  5885  ovtposg  5905  addpiord  6472  mulpiord  6473  addvalex  6978  cnref1o  8680  ioof  8941  frecuzrdgrrn  9358  frec2uzrdg  9359  frecuzrdgsuc  9365  cnrecnv  9738
  Copyright terms: Public domain W3C validator