Definition df-ov 5880

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 5913 and ovprc2 5914. 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 5881. (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 5877	. 2 class ( A F B )
5	1, 2	cop 3597	. . 3 class <. A , B >.
6	5, 3	cfv 5218	. 2 class ( F ` <. A , B >. )
7	4, 6	wceq 1353	1 wff ( A F B ) = ( F ` <. A , B >. )

This definition is referenced by:  oveq  5883  oveq1  5884  oveq2  5885  nfovd  5906  fnovex  5910  ovexg  5911  ovprc  5912  fnotovb  5920  ffnov  5981  eqfnov  5983  fnovim  5985  ovid  5993  ovidig  5994  ov  5996  ovigg  5997  ov6g  6014  ovg  6015  ovres  6016  fovcdm  6019  fnrnov  6022  foov  6023  fnovrn  6024  funimassov  6026  ovelimab  6027  ovconst2  6028  elmpocl  6071  oprssdmm  6174  mpofvex  6206  oprab2co  6221  algrflem  6232  algrflemg  6233  mpoxopn0yelv  6242  ovtposg  6262  addpiord  7317  mulpiord  7318  addvalex  7845  cnref1o  9652  ioof  9973  frecuzrdgrrn  10410  frec2uzrdg  10411  frecuzrdgrcl  10412  frecuzrdgsuc  10416  frecuzrdgrclt  10417  frecuzrdgg  10418  frecuzrdgsuctlem  10425  seq3val  10460  seqvalcd  10461  cnrecnv  10921  eucalgval  12056  eucalginv  12058  eucalglt  12059  eucalg  12061  sqpweven  12177  2sqpwodd  12178  isstructim  12478  isstructr  12479  imasaddvallemg  12741  xpsff1o  12773  mgm1  12794  sgrp1  12821  mnd1  12852  mnd1id  12853  grp1  12981  srgfcl  13161  ring1  13241  txdis1cn  13817  lmcn2  13819  cnmpt12f  13825  cnmpt21  13830  cnmpt2t  13832  cnmpt22  13833  psmetxrge0  13871  xmeterval  13974  comet  14038  txmetcnp  14057  qtopbasss  14060  cnmetdval  14068  remetdval  14078  tgqioo  14086