Definition df-ov 5439

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 5464 and ovprc2 5465. 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 5440. (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 5436	. 2 class (A𝐹B)
5	1, 2	cop 3353	. . 3 class ⟨A, B⟩
6	5, 3	cfv 4829	. 2 class (𝐹‘⟨A, B⟩)
7	4, 6	wceq 1228	1 wff (A𝐹B) = (𝐹‘⟨A, B⟩)

This definition is referenced by:  oveq  5442  oveq1  5443  oveq2  5444  nfovd  5458  fnovex  5462  ovprc  5463  fnotovb  5471  ffnov  5528  eqfnov  5530  fnovim  5532  ovid  5540  ovidig  5541  ov  5543  ovigg  5544  ov6g  5561  ovg  5562  ovres  5563  fovrn  5566  fnrnov  5569  foov  5570  fnovrn  5571  funimassov  5573  ovelimab  5574  ovconst2  5575  elmpt2cl  5621  mpt2fvex  5752  oprab2co  5762  algrflem  5773  mpt2xopn0yelv  5776  ovtposg  5796  addpiord  6176  mulpiord  6177