Definition df-ov 5535

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 5561 and ovprc2 5562. 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 5536. (Contributed by NM, 28-Feb-1995.)

Assertion

Ref	Expression
df-ov	⊢ (𝐴𝐹𝐵) = (𝐹‘⟨𝐴, 𝐵⟩)

Detailed syntax breakdown of Definition df-ov

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cB	. . 3 class 𝐵
3		cF	. . 3 class 𝐹
4	1, 2, 3	co 5532	. 2 class (𝐴𝐹𝐵)
5	1, 2	cop 3401	. . 3 class ⟨𝐴, 𝐵⟩
6	5, 3	cfv 4922	. 2 class (𝐹‘⟨𝐴, 𝐵⟩)
7	4, 6	wceq 1284	1 wff (𝐴𝐹𝐵) = (𝐹‘⟨𝐴, 𝐵⟩)

This definition is referenced by:  oveq  5538  oveq1  5539  oveq2  5540  nfovd  5554  fnovex  5558  ovexg  5559  ovprc  5560  fnotovb  5568  ffnov  5625  eqfnov  5627  fnovim  5629  ovid  5637  ovidig  5638  ov  5640  ovigg  5641  ov6g  5658  ovg  5659  ovres  5660  fovrn  5663  fnrnov  5666  foov  5667  fnovrn  5668  funimassov  5670  ovelimab  5671  ovconst2  5672  elmpt2cl  5718  mpt2fvex  5849  oprab2co  5859  algrflem  5870  algrflemg  5871  mpt2xopn0yelv  5877  ovtposg  5897  addpiord  6506  mulpiord  6507  addvalex  7012  cnref1o  8733  ioof  8994  frecuzrdgrrn  9410  frec2uzrdg  9411  frecuzrdgsuc  9417  cnrecnv  9797  eucalgval  10436  eucalginv  10438  eucalglt  10439  eucialg  10441  sqpweven  10553  2sqpwodd  10554