Definition df-ov 5844

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 𝐹 and its arguments 𝐴 and 𝐵- will be useful for proving meaningful theorems. For example, if class 𝐹 is the operation + and arguments 𝐴 and 𝐵 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 𝐴 and/or 𝐵 are proper classes (i.e. are not sets); see ovprc1 5874 and ovprc2 5875. On the other hand, we often find uses for this definition when 𝐹 is a proper class. 𝐹 is normally equal to a class of nested ordered pairs of the form defined by df-oprab 5845. (Contributed by NM, 28-Feb-1995.)

Assertion

Ref	Expression
df-ov	⊢ (𝐴𝐹𝐵) = (𝐹‘⟨𝐴, 𝐵⟩)

Detailed syntax breakdown of Definition df-ov

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cB	. . 3 class 𝐵
3		cF	. . 3 class 𝐹
4	1, 2, 3	co 5841	. 2 class (𝐴𝐹𝐵)
5	1, 2	cop 3578	. . 3 class ⟨𝐴, 𝐵⟩
6	5, 3	cfv 5187	. 2 class (𝐹‘⟨𝐴, 𝐵⟩)
7	4, 6	wceq 1343	1 wff (𝐴𝐹𝐵) = (𝐹‘⟨𝐴, 𝐵⟩)

This definition is referenced by:  oveq  5847  oveq1  5848  oveq2  5849  nfovd  5867  fnovex  5871  ovexg  5872  ovprc  5873  fnotovb  5881  ffnov  5942  eqfnov  5944  fnovim  5946  ovid  5954  ovidig  5955  ov  5957  ovigg  5958  ov6g  5975  ovg  5976  ovres  5977  fovrn  5980  fnrnov  5983  foov  5984  fnovrn  5985  funimassov  5987  ovelimab  5988  ovconst2  5989  elmpocl  6035  oprssdmm  6136  mpofvex  6168  oprab2co  6182  algrflem  6193  algrflemg  6194  mpoxopn0yelv  6203  ovtposg  6223  addpiord  7253  mulpiord  7254  addvalex  7781  cnref1o  9584  ioof  9903  frecuzrdgrrn  10339  frec2uzrdg  10340  frecuzrdgrcl  10341  frecuzrdgsuc  10345  frecuzrdgrclt  10346  frecuzrdgg  10347  frecuzrdgsuctlem  10354  seq3val  10389  seqvalcd  10390  cnrecnv  10848  eucalgval  11982  eucalginv  11984  eucalglt  11985  eucalg  11987  sqpweven  12103  2sqpwodd  12104  isstructim  12404  isstructr  12405  txdis1cn  12878  lmcn2  12880  cnmpt12f  12886  cnmpt21  12891  cnmpt2t  12893  cnmpt22  12894  psmetxrge0  12932  xmeterval  13035  comet  13099  txmetcnp  13118  qtopbasss  13121  cnmetdval  13129  remetdval  13139  tgqioo  13147