Definition df-ov 5671

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 5701 and ovprc2 5702. 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 5672. (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 5668	. 2 class (𝐴𝐹𝐵)
5	1, 2	cop 3455	. . 3 class ⟨𝐴, 𝐵⟩
6	5, 3	cfv 5030	. 2 class (𝐹‘⟨𝐴, 𝐵⟩)
7	4, 6	wceq 1290	1 wff (𝐴𝐹𝐵) = (𝐹‘⟨𝐴, 𝐵⟩)

This definition is referenced by:  oveq  5674  oveq1  5675  oveq2  5676  nfovd  5694  fnovex  5698  ovexg  5699  ovprc  5700  fnotovb  5708  ffnov  5765  eqfnov  5767  fnovim  5769  ovid  5777  ovidig  5778  ov  5780  ovigg  5781  ov6g  5798  ovg  5799  ovres  5800  fovrn  5803  fnrnov  5806  foov  5807  fnovrn  5808  funimassov  5810  ovelimab  5811  ovconst2  5812  elmpt2cl  5858  mpt2fvex  5989  oprab2co  5999  algrflem  6010  algrflemg  6011  mpt2xopn0yelv  6020  ovtposg  6040  addpiord  6938  mulpiord  6939  addvalex  7444  cnref1o  9196  ioof  9452  frecuzrdgrrn  9878  frec2uzrdg  9879  frecuzrdgrcl  9880  frecuzrdgsuc  9884  frecuzrdgrclt  9885  frecuzrdgg  9886  frecuzrdgsuctlem  9893  iseqvalt  9936  seq3val  9937  cnrecnv  10407  eucalgval  11377  eucalginv  11379  eucalglt  11380  eucalg  11382  sqpweven  11494  2sqpwodd  11495  isstructim  11571  isstructr  11572