Definition df-opr 3960

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 5964). This definition is well-defined, although not very meaningful, when classes A and/or B are proper classes (i.e. are not sets); see oprprc1 3979 and oprprc2 3980. On the other hand, we often find uses for this definition when F is a proper class, such as +_o in oav 4143. F is normally equal to a class of nested ordered pairs of the form defined by df-oprab 3961.

Assertion

Ref	Expression
df-opr	⊢ (AFB) = (F ‘⟨A, B⟩)

Detailed syntax breakdown of Definition df-opr

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cB	. . 3 class B
3		cF	. . 3 class F
4	1, 2, 3	co 3958	. 2 class (AFB)
5	1, 2	cop 2408	. . 3 class ⟨A, B⟩
6	5, 3	cfv 3178	. 2 class (F ‘⟨A, B⟩)
7	4, 6	wceq 955	1 wff (AFB) = (F ‘⟨A, B⟩)

This definition is referenced by:  opreq 3962  opreq1 3963  opreq2 3964  hbopr 3976  oprex 3978  oprprc1 3979  oprprc2 3980  ffnoprval 4009  eqfnoprval 4011  fnoprval 4012  oprabval 4018  oprabvalig 4019  oprabval6g 4027  oprvalres 4028  foprrn 4030  fnrnoprval 4031  fooprval 4032  fnoprvalrn 4033  oprvalconst2 4035  oprvalex 4036  oprssdm 4037  ndmoprg 4038  1st2val 4088  2nd2val 4089  curry1 4091  elrnoprabg 4117  addpiord 4995  mulpiord 4996  cnmetdval 7864  remetdval 7870  oprcn 7939  bopcnlem2 7944  bopcnlem3 7945  grpsn 8088  ringsn 8127  imsdval 8281  ipfval 8314  oprabvaligg 10399  fnoprvalrn2 10424  subsp 10488  1ded 10587  1cat 10608  ishomb 10632  isfuna 10664

Copyright terms: Public domain