Definition df-ov 5785

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 5815 and ovprc2 5816. 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 5786. (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 5782	. 2 class (𝐴𝐹𝐵)
5	1, 2	cop 3535	. . 3 class ⟨𝐴, 𝐵⟩
6	5, 3	cfv 5131	. 2 class (𝐹‘⟨𝐴, 𝐵⟩)
7	4, 6	wceq 1332	1 wff (𝐴𝐹𝐵) = (𝐹‘⟨𝐴, 𝐵⟩)

This definition is referenced by:  oveq  5788  oveq1  5789  oveq2  5790  nfovd  5808  fnovex  5812  ovexg  5813  ovprc  5814  fnotovb  5822  ffnov  5883  eqfnov  5885  fnovim  5887  ovid  5895  ovidig  5896  ov  5898  ovigg  5899  ov6g  5916  ovg  5917  ovres  5918  fovrn  5921  fnrnov  5924  foov  5925  fnovrn  5926  funimassov  5928  ovelimab  5929  ovconst2  5930  elmpocl  5976  oprssdmm  6077  mpofvex  6109  oprab2co  6123  algrflem  6134  algrflemg  6135  mpoxopn0yelv  6144  ovtposg  6164  addpiord  7148  mulpiord  7149  addvalex  7676  cnref1o  9469  ioof  9784  frecuzrdgrrn  10212  frec2uzrdg  10213  frecuzrdgrcl  10214  frecuzrdgsuc  10218  frecuzrdgrclt  10219  frecuzrdgg  10220  frecuzrdgsuctlem  10227  seq3val  10262  seqvalcd  10263  cnrecnv  10714  eucalgval  11771  eucalginv  11773  eucalglt  11774  eucalg  11776  sqpweven  11889  2sqpwodd  11890  isstructim  12012  isstructr  12013  txdis1cn  12486  lmcn2  12488  cnmpt12f  12494  cnmpt21  12499  cnmpt2t  12501  cnmpt22  12502  psmetxrge0  12540  xmeterval  12643  comet  12707  txmetcnp  12726  qtopbasss  12729  cnmetdval  12737  remetdval  12747  tgqioo  12755