Definition df-ov 5430

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 A and B- will be useful for proving meaningful theorems. For example, if class 𝐹 is the operation + and arguments A and B 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 A and/or B are proper classes (i.e. are not sets); see ovprc1 5455 and ovprc2 5456. 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 5431. (Contributed by NM, 28-Feb-1995.)

Assertion

Ref	Expression
df-ov	⊢ (A𝐹B) = (𝐹‘⟨A, B⟩)

Detailed syntax breakdown of Definition df-ov

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cB	. . 3 class B
3		cF	. . 3 class 𝐹
4	1, 2, 3	co 5427	. 2 class (A𝐹B)
5	1, 2	cop 3345	. . 3 class ⟨A, B⟩
6	5, 3	cfv 4820	. 2 class (𝐹‘⟨A, B⟩)
7	4, 6	wceq 1226	1 wff (A𝐹B) = (𝐹‘⟨A, B⟩)

This definition is referenced by:  oveq  5433  oveq1  5434  oveq2  5435  nfovd  5449  fnovex  5453  ovprc  5454  fnotovb  5462  ffnov  5519  eqfnov  5521  fnovim  5523  ovid  5531  ovidig  5532  ov  5534  ovigg  5535  ov6g  5552  ovg  5553  ovres  5554  fovrn  5557  fnrnov  5560  foov  5561  fnovrn  5562  funimassov  5564  ovelimab  5565  ovconst2  5566  elmpt2cl  5612  mpt2fvex  5743  oprab2co  5753  algrflem  5764  mpt2xopn0yelv  5767  ovtposg  5787  addpiord  6165  mulpiord  6166  ioof  8319