Definition df-ov 5891

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 5924 and ovprc2 5925. 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 5892. (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 5888	. 2 class (𝐴𝐹𝐵)
5	1, 2	cop 3607	. . 3 class ⟨𝐴, 𝐵⟩
6	5, 3	cfv 5228	. 2 class (𝐹‘⟨𝐴, 𝐵⟩)
7	4, 6	wceq 1363	1 wff (𝐴𝐹𝐵) = (𝐹‘⟨𝐴, 𝐵⟩)

This definition is referenced by:  oveq  5894  oveq1  5895  oveq2  5896  nfovd  5917  fnovex  5921  ovexg  5922  ovprc  5923  fnotovb  5931  ffnov  5992  eqfnov  5994  fnovim  5996  ovid  6004  ovidig  6005  ov  6007  ovigg  6008  ov6g  6025  ovg  6026  ovres  6027  fovcdm  6030  fnrnov  6033  foov  6034  fnovrn  6035  funimassov  6037  ovelimab  6038  ovconst2  6039  elmpocl  6082  oprssdmm  6185  mpofvex  6217  oprab2co  6232  algrflem  6243  algrflemg  6244  mpoxopn0yelv  6253  ovtposg  6273  addpiord  7328  mulpiord  7329  addvalex  7856  cnref1o  9663  ioof  9984  frecuzrdgrrn  10421  frec2uzrdg  10422  frecuzrdgrcl  10423  frecuzrdgsuc  10427  frecuzrdgrclt  10428  frecuzrdgg  10429  frecuzrdgsuctlem  10436  seq3val  10471  seqvalcd  10472  cnrecnv  10932  eucalgval  12067  eucalginv  12069  eucalglt  12070  eucalg  12072  sqpweven  12188  2sqpwodd  12189  isstructim  12489  isstructr  12490  imasaddvallemg  12753  xpsff1o  12786  mgm1  12807  sgrp1  12835  mnd1  12868  mnd1id  12869  grp1  13002  srgfcl  13220  ring1  13304  txdis1cn  14049  lmcn2  14051  cnmpt12f  14057  cnmpt21  14062  cnmpt2t  14064  cnmpt22  14065  psmetxrge0  14103  xmeterval  14206  comet  14270  txmetcnp  14289  qtopbasss  14292  cnmetdval  14300  remetdval  14310  tgqioo  14318