Definition df-ov 5856

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 5889 and ovprc2 5890. 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 5857. (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 5853	. 2 class (𝐴𝐹𝐵)
5	1, 2	cop 3586	. . 3 class ⟨𝐴, 𝐵⟩
6	5, 3	cfv 5198	. 2 class (𝐹‘⟨𝐴, 𝐵⟩)
7	4, 6	wceq 1348	1 wff (𝐴𝐹𝐵) = (𝐹‘⟨𝐴, 𝐵⟩)

This definition is referenced by:  oveq  5859  oveq1  5860  oveq2  5861  nfovd  5882  fnovex  5886  ovexg  5887  ovprc  5888  fnotovb  5896  ffnov  5957  eqfnov  5959  fnovim  5961  ovid  5969  ovidig  5970  ov  5972  ovigg  5973  ov6g  5990  ovg  5991  ovres  5992  fovrn  5995  fnrnov  5998  foov  5999  fnovrn  6000  funimassov  6002  ovelimab  6003  ovconst2  6004  elmpocl  6047  oprssdmm  6150  mpofvex  6182  oprab2co  6197  algrflem  6208  algrflemg  6209  mpoxopn0yelv  6218  ovtposg  6238  addpiord  7278  mulpiord  7279  addvalex  7806  cnref1o  9609  ioof  9928  frecuzrdgrrn  10364  frec2uzrdg  10365  frecuzrdgrcl  10366  frecuzrdgsuc  10370  frecuzrdgrclt  10371  frecuzrdgg  10372  frecuzrdgsuctlem  10379  seq3val  10414  seqvalcd  10415  cnrecnv  10874  eucalgval  12008  eucalginv  12010  eucalglt  12011  eucalg  12013  sqpweven  12129  2sqpwodd  12130  isstructim  12430  isstructr  12431  mgm1  12624  sgrp1  12651  mnd1  12679  mnd1id  12680  txdis1cn  13072  lmcn2  13074  cnmpt12f  13080  cnmpt21  13085  cnmpt2t  13087  cnmpt22  13088  psmetxrge0  13126  xmeterval  13229  comet  13293  txmetcnp  13312  qtopbasss  13315  cnmetdval  13323  remetdval  13333  tgqioo  13341