Definition df-ov 6299

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 and , the expression can be proved to equal (see 3p2e5 10693). This definition is well-defined, although not very meaningful, when classes and/or are proper classes (i.e. are not sets); see ovprc1 6327 and ovprc2 6328. On the other hand, we often find uses for this definition when is a proper class, such as in oav 7180. is normally equal to a class of nested ordered pairs of the form defined by df-oprab 6300. (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
2		cB	. . 3
3		cF	. . 3
4	1, 2, 3	co 6296	. 2
5	1, 2	cop 4035	. . 3
6	5, 3	cfv 5593	. 2
7	4, 6	wceq 1395	1

This definition is referenced by:  oveq  6302  oveq1  6303  oveq2  6304  nfovd  6321  ovex  6324  ovssunirn  6325  ovprc  6326  csbov123  6330  csbov  6331  elovimad  6337  fnotovb  6338  ffnov  6406  eqfnov  6408  fnov  6410  ovid  6419  ovidig  6420  ov  6422  ovigg  6423  ov6g  6440  ovg  6441  ovres  6442  fovrn  6445  fnrnov  6448  foov  6449  fnovrn  6450  funimassov  6452  ovelimab  6453  ovima0  6454  ovconst2  6455  oprssdm  6456  nssdmovg  6457  ndmovg  6458  elmpt2cl  6517  1st2val  6826  2nd2val  6827  bropopvvv  6880  ovmptss  6881  oprab2co  6885  curry1  6892  curry2  6895  algrflem  6909  mpt2xopn0yelv  6960  mpt2xopxnop0  6962  ovtpos  6989  mpt2curryd  7017  seqomlem1  7134  seqomlem4  7137  brwitnlem  7176  cantnfvalf  8105  fseqenlem1  8426  axdc4lem  8856  fpwwe  9045  canthwelem  9049  addpiord  9283  mulpiord  9284  addpqnq  9337  mulpqnq  9340  recmulnq  9363  dmrecnq  9367  cnref1o  11244  ixxssxr  11570  om2uzrdg  12067  uzrdgsuci  12071  swrd00  12645  swrd0  12658  cnrecnv  12998  sadcf  14103  smupf  14128  eucalgval  14211  eucalginv  14213  eucalglt  14214  eucalg  14216  vdwmc  14496  isstruct2  14641  isstruct  14642  imasaddvallem  14926  imasvscafn  14934  imasvscaval  14935  xpsff1o  14965  xpsaddlem  14972  xpsvsca  14976  xpsle  14978  comffval  15094  comfffval2  15096  comfeq  15101  isoval  15159  isssc  15189  isfuncd  15234  funcf2  15237  idfu2nd  15246  idfucl  15250  cofucl  15257  resfval2  15262  resf2nd  15264  funcres2b  15266  funcpropd  15269  homarcl  15355  homaval  15358  homarcl2  15362  arwhoma  15372  coapm  15398  catcco  15428  catcisolem  15433  xpcco  15452  xpcid  15458  xpcpropd  15477  evlfcllem  15490  evlfcl  15491  curf1cl  15497  curf2cl  15500  curfcl  15501  uncf1  15505  uncf2  15506  uncfcurf  15508  diag11  15512  diag12  15513  diag2  15514  curf2ndf  15516  hof2fval  15524  hofcl  15528  hofpropd  15536  yonedalem21  15542  yonedalem22  15547  yonedalem3b  15548  yonedalem3  15549  yonedainv  15550  yonffthlem  15551  joinval  15635  meetval  15649  plusffval  15877  mgm1  15884  sgrp1  15918  mnd1  15961  mnd1OLD  15962  mnd1id  15963  grp1  16142  gaid  16337  oppglsm  16662  efgmnvl  16732  efgval2  16742  vrgpinv  16787  frgpuptinv  16789  frgpuplem  16790  frgpup2  16794  frgpup3lem  16795  frgpnabllem1  16877  gsum2dlem1  16997  gsum2dlem2  16998  gsum2d  16999  gsum2dOLD  17000  gsum2d2lem  17001  gsumcom2  17003  eldprd  17035  eldprdOLD  17037  dprd2dlem2  17089  dprd2dlem1  17090  dprd2da  17091  ring1  17248  scaffval  17530  ply1frcl  18355  ipffval  18683  mamudi  18905  mamudir  18906  mamuvs1  18907  mamuvs2  18908  matplusgcell  18935  matsubgcell  18936  matvscacell  18938  mat1dimmul  18978  mat1rhmelval  18982  mdetrlin  19104  mdetrsca  19105  pmatcoe1fsupp  19202  iccordt  19715  iscnp2  19740  ptbasfi  20082  txcnpi  20109  txdis1cn  20136  lmcn2  20150  xkococn  20161  cnmpt12f  20167  cnmpt21  20172  cnmpt2t  20174  cnmpt22  20175  cnmpt2k  20189  xkohmeo  20316  flfcnp2  20508  tmdcn2  20588  clssubg  20607  tgphaus  20615  qustgplem  20619  psmetxrge0  20817  imasdsf1olem  20876  xpsdsval  20884  xmeterval  20935  comet  21016  txmetcnp  21050  metustidOLD  21062  metustid  21063  metustsymOLD  21064  metustsym  21065  metustexhalfOLD  21066  metustexhalf  21067  blval2  21078  metuel2  21082  nrmmetd  21095  nmfval  21109  isngp3  21118  ngpds  21123  tngnm  21165  qtopbaslem  21265  cnmetdval  21278  remetdval  21294  tgqioo  21305  bndth  21458  htpyco2  21479  phtpyco2  21490  caubl  21746  caublcls  21747  bcthlem1  21763  bcthlem2  21764  bcthlem4  21766  bcthlem5  21767  ovolfioo  21879  ovolficc  21880  ovolficcss  21881  ovolfsval  21882  ovolctb  21901  ovoliunlem2  21914  ovolicc2lem1  21928  ovolicc2lem5  21932  ovolfs2  21980  ioorinv  21985  uniiccdif  21987  uniioovol  21988  uniiccvol  21989  uniioombllem2a  21991  uniioombllem2  21992  uniioombllem3a  21993  uniioombllem3  21994  uniioombllem4  21995  uniioombllem5  21996  uniioombllem6  21997  dyadovol  22002  dyadss  22003  dyaddisjlem  22004  dyadmaxlem  22006  dyadmbl  22009  opnmbllem  22010  itg1addlem4  22106  limccnp2  22296  dvbsss  22306  perfdvf  22307  dvdsmulf1o  23470  fsumdvdsmul  23471  fsumvma  23488  tglngne  23937  ltgseg  23982  tgelrnln  24010  edgov  24341  usgraexmplvtx  24402  usgraexmplcvtx  24405  usgraexmplcedg  24406  2wlkonot3v  24875  2spthonot3v  24876  isrgrac  24934  grposn  25217  rngosn  25406  imsdval  25592  ofresid  27482  ofoprabco  27505  xrofsup  27582  fvproj  27835  logb2aval  28009  elunirnmbfm  28224  sibfof  28282  oddpwdcv  28294  eulerpartlemgh  28317  cndprobval  28372  cvmlift2lem9  28756  cvmlift2lem10  28757  cvmlift2lem13  28760  cvmliftphtlem  28762  mclsrcl  28921  fvtransport  29682  fvray  29791  linedegen  29793  fvline  29794  opnmbllem0  30050  mblfinlem1  30051  mblfinlem2  30052  ftc1anc  30098  ftc2nc  30099  opropabco  30214  f1opr  30215  ismtyhmeolem  30300  heiborlem3  30309  heiborlem4  30310  heiborlem6  30312  heiborlem8  30314  fourierdlem42  31931  aovfundmoveq  32266  aovpcov0  32275  aovnuoveq  32276  aovvoveq  32277  aov0ov0  32278  aovovn0oveq  32279  aov0nbovbi  32280  aovov0bi  32281  uhgrasize  32393  usgrafisbaseALT  32440  usgrafisbaseALT2  32441  usgfis  32446  usgfisALT  32450  ovn0dmfun  32452  ovn0ssdmfun  32455  plusfreseq  32460  brcic  32582  idfusubc0  32591  rhmsubclem2  32895  rhmsubcOLDlem2  32914  lmod1lem2  33089  lmod1lem3  33090  bj-finsumval0  34663