Definition df-ov 5777

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 5807 and ovprc2 5808. 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 5778. (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 5774	. 2 class ( A F B )
5	1, 2	cop 3530	. . 3 class <. A , B >.
6	5, 3	cfv 5123	. 2 class ( F ` <. A , B >. )
7	4, 6	wceq 1331	1 wff ( A F B ) = ( F ` <. A , B >. )

This definition is referenced by:  oveq  5780  oveq1  5781  oveq2  5782  nfovd  5800  fnovex  5804  ovexg  5805  ovprc  5806  fnotovb  5814  ffnov  5875  eqfnov  5877  fnovim  5879  ovid  5887  ovidig  5888  ov  5890  ovigg  5891  ov6g  5908  ovg  5909  ovres  5910  fovrn  5913  fnrnov  5916  foov  5917  fnovrn  5918  funimassov  5920  ovelimab  5921  ovconst2  5922  elmpocl  5968  oprssdmm  6069  mpofvex  6101  oprab2co  6115  algrflem  6126  algrflemg  6127  mpoxopn0yelv  6136  ovtposg  6156  addpiord  7124  mulpiord  7125  addvalex  7652  cnref1o  9440  ioof  9754  frecuzrdgrrn  10181  frec2uzrdg  10182  frecuzrdgrcl  10183  frecuzrdgsuc  10187  frecuzrdgrclt  10188  frecuzrdgg  10189  frecuzrdgsuctlem  10196  seq3val  10231  seqvalcd  10232  cnrecnv  10682  eucalgval  11735  eucalginv  11737  eucalglt  11738  eucalg  11740  sqpweven  11853  2sqpwodd  11854  isstructim  11973  isstructr  11974  txdis1cn  12447  lmcn2  12449  cnmpt12f  12455  cnmpt21  12460  cnmpt2t  12462  cnmpt22  12463  psmetxrge0  12501  xmeterval  12604  comet  12668  txmetcnp  12687  qtopbasss  12690  cnmetdval  12698  remetdval  12708  tgqioo  12716