Definition df-ov 5853

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 5886 and ovprc2 5887. 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 5854. (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 5850	. 2 class ( A F B )
5	1, 2	cop 3584	. . 3 class <. A , B >.
6	5, 3	cfv 5196	. 2 class ( F ` <. A , B >. )
7	4, 6	wceq 1348	1 wff ( A F B ) = ( F ` <. A , B >. )

This definition is referenced by:  oveq  5856  oveq1  5857  oveq2  5858  nfovd  5879  fnovex  5883  ovexg  5884  ovprc  5885  fnotovb  5893  ffnov  5954  eqfnov  5956  fnovim  5958  ovid  5966  ovidig  5967  ov  5969  ovigg  5970  ov6g  5987  ovg  5988  ovres  5989  fovrn  5992  fnrnov  5995  foov  5996  fnovrn  5997  funimassov  5999  ovelimab  6000  ovconst2  6001  elmpocl  6044  oprssdmm  6147  mpofvex  6179  oprab2co  6194  algrflem  6205  algrflemg  6206  mpoxopn0yelv  6215  ovtposg  6235  addpiord  7265  mulpiord  7266  addvalex  7793  cnref1o  9596  ioof  9915  frecuzrdgrrn  10351  frec2uzrdg  10352  frecuzrdgrcl  10353  frecuzrdgsuc  10357  frecuzrdgrclt  10358  frecuzrdgg  10359  frecuzrdgsuctlem  10366  seq3val  10401  seqvalcd  10402  cnrecnv  10861  eucalgval  11995  eucalginv  11997  eucalglt  11998  eucalg  12000  sqpweven  12116  2sqpwodd  12117  isstructim  12417  isstructr  12418  mgm1  12611  sgrp1  12638  mnd1  12666  mnd1id  12667  txdis1cn  13031  lmcn2  13033  cnmpt12f  13039  cnmpt21  13044  cnmpt2t  13046  cnmpt22  13047  psmetxrge0  13085  xmeterval  13188  comet  13252  txmetcnp  13271  qtopbasss  13274  cnmetdval  13282  remetdval  13292  tgqioo  13300