MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-ov Unicode version

Definition df-ov 5760
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  F and its arguments  A and  B- will be useful for proving meaningful theorems. For example, if class  F is the operation  + and arguments  A and  B are  3 and  2, the expression  ( 3  +  2 ) can be proved to equal  5 (see 3p2e5 9787). This definition is well-defined, although not very meaningful, when classes  A and/or  B are proper classes (i.e. are not sets); see ovprc1 5785 and ovprc2 5786. On the other hand, we often find uses for this definition when  F is a proper class, such as  +o in oav 6443.  F is normally equal to a class of nested ordered pairs of the form defined by df-oprab 5761. (Contributed by NM, 28-Feb-1995.)
Assertion
Ref Expression
df-ov  |-  ( A F B )  =  ( F `  <. A ,  B >. )

Detailed syntax breakdown of Definition df-ov
StepHypRef Expression
1 cA . . 3  class  A
2 cB . . 3  class  B
3 cF . . 3  class  F
41, 2, 3co 5757 . 2  class  ( A F B )
51, 2cop 3584 . . 3  class  <. A ,  B >.
65, 3cfv 4638 . 2  class  ( F `
 <. A ,  B >. )
74, 6wceq 1619 1  wff  ( A F B )  =  ( F `  <. A ,  B >. )
Colors of variables: wff set class
This definition is referenced by:  oveq  5763  oveq1  5764  oveq2  5765  nfovd  5779  ovex  5782  ovssunirn  5783  ovprc  5784  fnotovb  5793  ffnov  5847  eqfnov  5849  fnov  5851  ovid  5863  ovidig  5864  ov  5866  ovigg  5867  ov6g  5884  ovg  5885  ovres  5886  fovrn  5889  fnrnov  5892  foov  5893  fnovrn  5894  funimassov  5896  ovelimab  5897  ovconst2  5898  oprssdm  5901  ndmovg  5902  elmpt2cl  5960  1st2val  6044  2nd2val  6045  ovmptss  6099  oprab2co  6103  curry1  6109  curry2  6112  algrflem  6123  ovtpos  6148  seqomlem1  6395  seqomlem4  6398  brwitnlem  6439  cantnfvalf  7299  fseqenlem1  7584  axdc4lem  8014  fpwwe  8201  canthwelem  8205  addpiord  8441  mulpiord  8442  addpqnq  8495  mulpqnq  8498  recmulnq  8521  dmrecnq  8525  cnref1o  10281  ixxssxr  10599  om2uzrdg  10950  uzrdgsuci  10954  swrd00  11381  cnrecnv  11580  sadcf  12571  smupf  12596  eucalgval  12679  eucalginv  12681  eucalglt  12682  eucalg  12684  vdwmc  12952  isstruct2  13084  isstruct  13085  prdsval  13282  prdsplusg  13285  prdsmulr  13286  prdsvsca  13287  prdshom  13293  imasaddvallem  13358  imasvscafn  13366  imasvscaval  13367  xpsff1o  13397  xpsaddlem  13404  xpsvsca  13408  xpsle  13410  comffval  13529  comfffval2  13531  comfeq  13536  isoval  13594  isssc  13624  isfuncd  13666  funcf2  13669  idfu2nd  13678  idfucl  13682  cofucl  13689  resfval2  13694  resf2nd  13696  funcres2b  13698  funcpropd  13701  homarcl  13787  homaval  13790  homarcl2  13794  arwhoma  13804  coapm  13830  catcco  13860  catcisolem  13865  xpcco  13884  xpcid  13890  xpcpropd  13909  evlfcllem  13922  evlfcl  13923  curf1cl  13929  curf2cl  13932  curfcl  13933  uncf1  13937  uncf2  13938  uncfcurf  13940  diag11  13944  diag12  13945  diag2  13946  curf2ndf  13948  hof2fval  13956  hofcl  13960  hofpropd  13968  yonedalem21  13974  yonedalem22  13979  yonedalem3b  13980  yonedalem3  13981  yonedainv  13982  yonffthlem  13983  plusffval  14306  gaid  14680  oppglsm  14880  efgmnvl  14950  efgval2  14960  vrgpinv  15005  frgpuptinv  15007  frgpuplem  15008  frgpup2  15012  frgpup3lem  15013  frgpnabllem1  15088  gsum2d  15150  gsum2d2lem  15151  gsumcom2  15153  eldprd  15166  dprd2dlem2  15202  dprd2dlem1  15203  dprd2da  15204  scaffval  15572  ipffval  16479  iccordt  16871  iscnp2  16896  ptbasfi  17203  txcnpi  17229  txdis1cn  17256  lmcn2  17270  xkococn  17281  cnmpt12f  17287  cnmpt21  17292  cnmpt2t  17294  cnmpt22  17295  cnmpt2k  17309  xkohmeo  17433  flfcnp2  17629  tmdcn2  17699  clssubg  17718  tgphaus  17726  divstgplem  17730  imasdsf1olem  17864  xpsdsval  17872  xmeterval  17905  comet  17986  txmetcnp  18020  nrmmetd  18024  nmfval  18038  isngp3  18047  ngpds  18052  tngnm  18094  qtopbaslem  18194  cnmetdval  18207  remetdval  18222  tgqioo  18233  bndth  18383  htpyco2  18404  phtpyco2  18415  caubl  18660  caublcls  18661  bcthlem1  18673  bcthlem2  18674  bcthlem4  18676  bcthlem5  18677  ovolfioo  18754  ovolficc  18755  ovolficcss  18756  ovolfsval  18757  ovolctb  18776  ovoliunlem2  18789  ovolicc2lem1  18803  ovolicc2lem5  18807  ovolfs2  18853  ioorinv  18858  uniiccdif  18860  uniioovol  18861  uniiccvol  18862  uniioombllem2a  18864  uniioombllem2  18865  uniioombllem3a  18866  uniioombllem3  18867  uniioombllem4  18868  uniioombllem5  18869  uniioombllem6  18870  dyadovol  18875  dyadss  18876  dyaddisjlem  18877  dyadmaxlem  18879  dyadmbl  18882  opnmbllem  18883  itg1addlem4  18981  limccnp2  19169  dvbsss  19179  perfdvf  19180  dvdsmulf1o  20361  fsumdvdsmul  20362  fsumvma  20379  grposn  20807  rngosn  20996  imsdval  21180  cvmlift2lem9  23179  cvmlift2lem10  23180  cvmlift2lem13  23183  cvmliftphtlem  23185  fvtransport  23995  fvray  24104  linedegen  24106  fvline  24107  oprssopvg  24365  fnovpop  24369  fnovrn2  24381  cbcpcp  24494  ltrcmp  24737  islimrs  24912  vecaddonto  24991  vecscmonto  25018  1ded  25070  1cat  25091  ishomb  25120  isfuna  25166  valtar  25215  cmpmor  25307  opropabco  25721  f1opr  25723  ismtyhmeolem  25860  heiborlem3  25869  heiborlem4  25870  heiborlem6  25872  heiborlem8  25874  mamudi  26793  mamudir  26794  mamuvs1  26795  mamuvs2  26796  matrcl  26798  logbval  27272
  Copyright terms: Public domain W3C validator