Definition df-ov 5878

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 5911 and ovprc2 5912. 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 5879. (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 5875	. 2 class (𝐴𝐹𝐵)
5	1, 2	cop 3596	. . 3 class ⟨𝐴, 𝐵⟩
6	5, 3	cfv 5217	. 2 class (𝐹‘⟨𝐴, 𝐵⟩)
7	4, 6	wceq 1353	1 wff (𝐴𝐹𝐵) = (𝐹‘⟨𝐴, 𝐵⟩)

This definition is referenced by:  oveq  5881  oveq1  5882  oveq2  5883  nfovd  5904  fnovex  5908  ovexg  5909  ovprc  5910  fnotovb  5918  ffnov  5979  eqfnov  5981  fnovim  5983  ovid  5991  ovidig  5992  ov  5994  ovigg  5995  ov6g  6012  ovg  6013  ovres  6014  fovcdm  6017  fnrnov  6020  foov  6021  fnovrn  6022  funimassov  6024  ovelimab  6025  ovconst2  6026  elmpocl  6069  oprssdmm  6172  mpofvex  6204  oprab2co  6219  algrflem  6230  algrflemg  6231  mpoxopn0yelv  6240  ovtposg  6260  addpiord  7315  mulpiord  7316  addvalex  7843  cnref1o  9650  ioof  9971  frecuzrdgrrn  10408  frec2uzrdg  10409  frecuzrdgrcl  10410  frecuzrdgsuc  10414  frecuzrdgrclt  10415  frecuzrdgg  10416  frecuzrdgsuctlem  10423  seq3val  10458  seqvalcd  10459  cnrecnv  10919  eucalgval  12054  eucalginv  12056  eucalglt  12057  eucalg  12059  sqpweven  12175  2sqpwodd  12176  isstructim  12476  isstructr  12477  imasaddvallemg  12736  xpsff1o  12768  mgm1  12789  sgrp1  12816  mnd1  12847  mnd1id  12848  grp1  12976  srgfcl  13156  ring1  13236  txdis1cn  13781  lmcn2  13783  cnmpt12f  13789  cnmpt21  13794  cnmpt2t  13796  cnmpt22  13797  psmetxrge0  13835  xmeterval  13938  comet  14002  txmetcnp  14021  qtopbasss  14024  cnmetdval  14032  remetdval  14042  tgqioo  14050