Definition df-ov 5899

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 5932 and ovprc2 5933. 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 5900. (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 5896	. 2 class ( A F B )
5	1, 2	cop 3610	. . 3 class <. A , B >.
6	5, 3	cfv 5235	. 2 class ( F ` <. A , B >. )
7	4, 6	wceq 1364	1 wff ( A F B ) = ( F ` <. A , B >. )

This definition is referenced by:  oveq  5902  oveq1  5903  oveq2  5904  nfovd  5925  fnovex  5929  ovexg  5930  ovprc  5931  fnotovb  5939  ffnov  6000  eqfnov  6003  fnovim  6005  ovid  6013  ovidig  6014  ov  6016  ovigg  6017  ov6g  6034  ovg  6035  ovres  6036  fovcdm  6039  fnrnov  6042  foov  6043  fnovrn  6044  funimassov  6046  ovelimab  6047  ovconst2  6048  elmpocl  6091  oprssdmm  6196  mpofvex  6228  oprab2co  6243  algrflem  6254  algrflemg  6255  mpoxopn0yelv  6264  ovtposg  6284  addpiord  7345  mulpiord  7346  addvalex  7873  cnref1o  9680  ioof  10001  frecuzrdgrrn  10439  frec2uzrdg  10440  frecuzrdgrcl  10441  frecuzrdgsuc  10445  frecuzrdgrclt  10446  frecuzrdgg  10447  frecuzrdgsuctlem  10454  seq3val  10489  seqvalcd  10490  cnrecnv  10951  eucalgval  12086  eucalginv  12088  eucalglt  12089  eucalg  12091  sqpweven  12207  2sqpwodd  12208  isstructim  12526  isstructr  12527  relelbasov  12574  imasaddvallemg  12792  xpsff1o  12825  mgm1  12846  sgrp1  12874  mnd1  12907  mnd1id  12908  grp1  13050  srgfcl  13327  ring1  13411  txdis1cn  14235  lmcn2  14237  cnmpt12f  14243  cnmpt21  14248  cnmpt2t  14250  cnmpt22  14251  psmetxrge0  14289  xmeterval  14392  comet  14456  txmetcnp  14475  qtopbasss  14478  cnmetdval  14486  remetdval  14496  tgqioo  14504