Definition df-ov 5493

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 5519 and ovprc2 5520. 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 5494. (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 5490	. 2 class (𝐴𝐹𝐵)
5	1, 2	cop 3375	. . 3 class ⟨𝐴, 𝐵⟩
6	5, 3	cfv 4880	. 2 class (𝐹‘⟨𝐴, 𝐵⟩)
7	4, 6	wceq 1243	1 wff (𝐴𝐹𝐵) = (𝐹‘⟨𝐴, 𝐵⟩)

This definition is referenced by:  oveq  5496  oveq1  5497  oveq2  5498  nfovd  5512  fnovex  5516  ovexg  5517  ovprc  5518  fnotovb  5526  ffnov  5583  eqfnov  5585  fnovim  5587  ovid  5595  ovidig  5596  ov  5598  ovigg  5599  ov6g  5616  ovg  5617  ovres  5618  fovrn  5621  fnrnov  5624  foov  5625  fnovrn  5626  funimassov  5628  ovelimab  5629  ovconst2  5630  elmpt2cl  5676  mpt2fvex  5807  oprab2co  5817  algrflem  5828  algrflemg  5829  mpt2xopn0yelv  5832  ovtposg  5852  addpiord  6386  mulpiord  6387  addvalex  6892  cnref1o  8544  ioof  8798  frecuzrdgrrn  9063  frec2uzrdg  9064  frecuzrdgsuc  9070  cnrecnv  9379