Definition df-ov 5458

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 5483 and ovprc2 5484. 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 5459. (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 5455	. 2 class (A𝐹B)
5	1, 2	cop 3370	. . 3 class ⟨A, B⟩
6	5, 3	cfv 4845	. 2 class (𝐹‘⟨A, B⟩)
7	4, 6	wceq 1242	1 wff (A𝐹B) = (𝐹‘⟨A, B⟩)

This definition is referenced by:  oveq  5461  oveq1  5462  oveq2  5463  nfovd  5477  fnovex  5481  ovprc  5482  fnotovb  5490  ffnov  5547  eqfnov  5549  fnovim  5551  ovid  5559  ovidig  5560  ov  5562  ovigg  5563  ov6g  5580  ovg  5581  ovres  5582  fovrn  5585  fnrnov  5588  foov  5589  fnovrn  5590  funimassov  5592  ovelimab  5593  ovconst2  5594  elmpt2cl  5640  mpt2fvex  5771  oprab2co  5781  algrflem  5792  mpt2xopn0yelv  5795  ovtposg  5815  addpiord  6300  mulpiord  6301  cnref1o  8337  ioof  8590  frecuzrdgrrn  8855  frec2uzrdg  8856  frecuzrdgsuc  8862  cnrecnv  9118