Definition df-ov 5527

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 5529. (Contributed by SF, 5-Jan-2015.)

Assertion

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

Detailed syntax breakdown of Definition df-ov

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

This definition is referenced by:  oveq  5530  oveq1  5531  oveq2  5532  nfovd  5545  ovex  5552  fnopovb  5558  ffnov  5588  eqfnov  5590  fnov  5592  ovidig  5594  ov  5596  ovigg  5597  ov6g  5601  ovg  5602  ovres  5603  fovrn  5605  fnrnov  5606  foov  5607  fnovrn  5608  funimassov  5610  ovelimab  5611  ovconst2  5612  oprssdm  5613  ndmovg  5614  ndmovcl  5615  ndmov  5616  elovex12  5649  brcupg  5815  brcomposeg  5820  braddcfn  5827  brcrossg  5849  brfullfunop  5868  fce  6189