Definition df-ov 5618

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 F and its arguments A and B- will be useful for proving meaningful theorems. For example, if class F 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 5644 and ovprc2 5645. On the other hand, we often find uses for this definition when F is a proper class. F is normally equal to a class of nested ordered pairs of the form defined by df-oprab 5619. (Contributed by NM, 28-Feb-1995.)

Assertion

Ref	Expression
df-ov	|- ( A F B ) = ( F ` <. 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 F
4	1, 2, 3	co 5615	. 2 class ( A F B )
5	1, 2	cop 3434	. . 3 class <. A , B >.
6	5, 3	cfv 4983	. 2 class ( F ` <. A , B >. )
7	4, 6	wceq 1287	1 wff ( A F B ) = ( F ` <. A , B >. )

This definition is referenced by:  oveq  5621  oveq1  5622  oveq2  5623  nfovd  5637  fnovex  5641  ovexg  5642  ovprc  5643  fnotovb  5651  ffnov  5708  eqfnov  5710  fnovim  5712  ovid  5720  ovidig  5721  ov  5723  ovigg  5724  ov6g  5741  ovg  5742  ovres  5743  fovrn  5746  fnrnov  5749  foov  5750  fnovrn  5751  funimassov  5753  ovelimab  5754  ovconst2  5755  elmpt2cl  5801  mpt2fvex  5932  oprab2co  5942  algrflem  5953  algrflemg  5954  mpt2xopn0yelv  5960  ovtposg  5980  addpiord  6822  mulpiord  6823  addvalex  7328  cnref1o  9068  ioof  9324  frecuzrdgrrn  9746  frec2uzrdg  9747  frecuzrdgrcl  9748  frecuzrdgsuc  9752  frecuzrdgrclt  9753  frecuzrdgg  9754  frecuzrdgsuctlem  9761  iseqvalt  9793  cnrecnv  10243  eucalgval  10942  eucalginv  10944  eucalglt  10945  eucialg  10947  sqpweven  11059  2sqpwodd  11060