NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  df-ov GIF version

Definition df-ov 5526
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. 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. F is normally equal to a class of nested ordered pairs of the form defined by df-oprab 5528. (Contributed by SF, 5-Jan-2015.)
Assertion
Ref Expression
df-ov (AFB) = (FA, 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 5525 . 2 class (AFB)
51, 2cop 4561 . . 3 class A, B
65, 3cfv 4781 . 2 class (FA, B)
74, 6wceq 1642 1 wff (AFB) = (FA, B)
Colors of variables: wff setvar class
This definition is referenced by:  oveq  5529  oveq1  5530  oveq2  5531  nfovd  5544  ovex  5551  fnopovb  5557  ffnov  5587  eqfnov  5589  fnov  5591  ovidig  5593  ov  5595  ovigg  5596  ov6g  5600  ovg  5601  ovres  5602  fovrn  5604  fnrnov  5605  foov  5606  fnovrn  5607  funimassov  5609  ovelimab  5610  ovconst2  5611  oprssdm  5612  ndmovg  5613  ndmovcl  5614  ndmov  5615  elovex12  5648  brcupg  5814  brcomposeg  5819  braddcfn  5826  brcrossg  5848  brfullfunop  5867  fce  6188
  Copyright terms: Public domain W3C validator