Definition df-opr 3003

Description: Define the result of an operation. Note that the syntax is simply three class symbols in a row bracketed by parentheses. Definition of [Enderton] p. 79. Class F normally denotes an operation such as + that operates on two classes A and B, which might be numbers such as 1 and 2. This definition is well-defined, although not very meaningful, when classes A and/or B are proper classes (i.e. are not sets). On the other hand we often find uses for this definition when F is a proper class.

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 3001	. 2 class (AFB)
5	1, 2	cop 1810	. . 3 class ⟨A, B⟩
6	5, 3	cfv 2422	. 2 class (F ‘⟨A, B⟩)
7	4, 6	wceq 1091	1 wff (AFB) = (F ‘⟨A, B⟩)

This definition is referenced by:  opreq 3005  opreq1 3006  opreq2 3007  hbopr 3017  oprex 3018  oprprc1 3019  oprprc2 3020  ffnoprval 3041  fnoprval 3042  oprabval 3047  oprabvalig 3048  elrnoprab 3054  oprvalex 3055  oprssdm 3056  ndmoprg 3057  1st2val 3097  addpiord 3806  mulpiord 3807

metamath.org