Definition df-ov 5709

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 5739 and ovprc2 5740. 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 5710. (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 5706	. 2 class ( A F B )
5	1, 2	cop 3477	. . 3 class <. A , B >.
6	5, 3	cfv 5059	. 2 class ( F ` <. A , B >. )
7	4, 6	wceq 1299	1 wff ( A F B ) = ( F ` <. A , B >. )

This definition is referenced by:  oveq  5712  oveq1  5713  oveq2  5714  nfovd  5732  fnovex  5736  ovexg  5737  ovprc  5738  fnotovb  5746  ffnov  5807  eqfnov  5809  fnovim  5811  ovid  5819  ovidig  5820  ov  5822  ovigg  5823  ov6g  5840  ovg  5841  ovres  5842  fovrn  5845  fnrnov  5848  foov  5849  fnovrn  5850  funimassov  5852  ovelimab  5853  ovconst2  5854  elmpocl  5900  mpofvex  6031  oprab2co  6045  algrflem  6056  algrflemg  6057  mpoxopn0yelv  6066  ovtposg  6086  addpiord  7025  mulpiord  7026  addvalex  7531  cnref1o  9290  ioof  9595  frecuzrdgrrn  10022  frec2uzrdg  10023  frecuzrdgrcl  10024  frecuzrdgsuc  10028  frecuzrdgrclt  10029  frecuzrdgg  10030  frecuzrdgsuctlem  10037  seq3val  10072  seqvalcd  10073  cnrecnv  10523  eucalgval  11528  eucalginv  11530  eucalglt  11531  eucalg  11533  sqpweven  11645  2sqpwodd  11646  isstructim  11755  isstructr  11756  txdis1cn  12228  lmcn2  12230  cnmpt12f  12236  cnmpt21  12241  cnmpt2t  12243  cnmpt22  12244  psmetxrge0  12260  xmeterval  12363  comet  12427  qtopbasss  12443  cnmetdval  12451  remetdval  12458  tgqioo  12466