Definition df-ov 5515

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 5541 and ovprc2 5542. 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 5516. (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 5512	. 2 class (𝐴𝐹𝐵)
5	1, 2	cop 3378	. . 3 class ⟨𝐴, 𝐵⟩
6	5, 3	cfv 4902	. 2 class (𝐹‘⟨𝐴, 𝐵⟩)
7	4, 6	wceq 1243	1 wff (𝐴𝐹𝐵) = (𝐹‘⟨𝐴, 𝐵⟩)

This definition is referenced by:  oveq  5518  oveq1  5519  oveq2  5520  nfovd  5534  fnovex  5538  ovexg  5539  ovprc  5540  fnotovb  5548  ffnov  5605  eqfnov  5607  fnovim  5609  ovid  5617  ovidig  5618  ov  5620  ovigg  5621  ov6g  5638  ovg  5639  ovres  5640  fovrn  5643  fnrnov  5646  foov  5647  fnovrn  5648  funimassov  5650  ovelimab  5651  ovconst2  5652  elmpt2cl  5698  mpt2fvex  5829  oprab2co  5839  algrflem  5850  algrflemg  5851  mpt2xopn0yelv  5854  ovtposg  5874  addpiord  6414  mulpiord  6415  addvalex  6920  cnref1o  8582  ioof  8840  frecuzrdgrrn  9194  frec2uzrdg  9195  frecuzrdgsuc  9201  cnrecnv  9510