Definition df-ov 5921

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 5954 and ovprc2 5955. 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 5922. (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 5918	. 2 class ( A F B )
5	1, 2	cop 3621	. . 3 class <. A , B >.
6	5, 3	cfv 5254	. 2 class ( F ` <. A , B >. )
7	4, 6	wceq 1364	1 wff ( A F B ) = ( F ` <. A , B >. )

This definition is referenced by:  oveq  5924  oveq1  5925  oveq2  5926  nfovd  5947  fnovex  5951  ovexg  5952  ovprc  5953  fnotovb  5961  ffnov  6022  eqfnov  6025  fnovim  6027  ovid  6035  ovidig  6036  ov  6038  ovigg  6039  ov6g  6056  ovg  6057  ovres  6058  fovcdm  6061  fnrnov  6064  foov  6065  fnovrn  6066  funimassov  6068  ovelimab  6069  ovconst2  6070  elmpocl  6113  oprssdmm  6224  mpofvex  6256  oprab2co  6271  algrflem  6282  algrflemg  6283  mpoxopn0yelv  6292  ovtposg  6312  addpiord  7376  mulpiord  7377  addvalex  7904  cnref1o  9716  ioof  10037  frecuzrdgrrn  10479  frec2uzrdg  10480  frecuzrdgrcl  10481  frecuzrdgsuc  10485  frecuzrdgrclt  10486  frecuzrdgg  10487  frecuzrdgsuctlem  10494  seq3val  10531  seqvalcd  10532  cnrecnv  11054  eucalgval  12192  eucalginv  12194  eucalglt  12195  eucalg  12197  sqpweven  12313  2sqpwodd  12314  isstructim  12632  isstructr  12633  relelbasov  12680  imasaddvallemg  12898  xpsff1o  12932  mgm1  12953  sgrp1  12994  mnd1  13027  mnd1id  13028  grp1  13178  srgfcl  13469  ring1  13555  txdis1cn  14446  lmcn2  14448  cnmpt12f  14454  cnmpt21  14459  cnmpt2t  14461  cnmpt22  14462  psmetxrge0  14500  xmeterval  14603  comet  14667  txmetcnp  14686  qtopbasss  14689  cnmetdval  14697  remetdval  14707  tgqioo  14715