Definition df-ov 5922

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 5955 and ovprc2 5956. 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 5923. (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 5919	. 2 class (𝐴𝐹𝐵)
5	1, 2	cop 3622	. . 3 class ⟨𝐴, 𝐵⟩
6	5, 3	cfv 5255	. 2 class (𝐹‘⟨𝐴, 𝐵⟩)
7	4, 6	wceq 1364	1 wff (𝐴𝐹𝐵) = (𝐹‘⟨𝐴, 𝐵⟩)

This definition is referenced by:  oveq  5925  oveq1  5926  oveq2  5927  nfovd  5948  fnovex  5952  ovexg  5953  ovprc  5954  fnotovb  5962  ffnov  6023  eqfnov  6026  fnovim  6028  ovid  6036  ovidig  6037  ov  6039  ovigg  6040  fvmpopr2d  6056  ov6g  6058  ovg  6059  ovres  6060  fovcdm  6063  fnrnov  6066  foov  6067  fnovrn  6068  funimassov  6070  ovelimab  6071  ovconst2  6072  elmpocl  6115  oprssdmm  6226  mpofvex  6260  oprab2co  6273  algrflem  6284  algrflemg  6285  mpoxopn0yelv  6294  ovtposg  6314  addpiord  7378  mulpiord  7379  addvalex  7906  cnref1o  9719  ioof  10040  frecuzrdgrrn  10482  frec2uzrdg  10483  frecuzrdgrcl  10484  frecuzrdgsuc  10488  frecuzrdgrclt  10489  frecuzrdgg  10490  frecuzrdgsuctlem  10497  seq3val  10534  seqvalcd  10535  cnrecnv  11057  eucalgval  12195  eucalginv  12197  eucalglt  12198  eucalg  12200  sqpweven  12316  2sqpwodd  12317  isstructim  12635  isstructr  12636  relelbasov  12683  imasaddvallemg  12901  xpsff1o  12935  mgm1  12956  sgrp1  12997  mnd1  13030  mnd1id  13031  grp1  13181  srgfcl  13472  ring1  13558  txdis1cn  14457  lmcn2  14459  cnmpt12f  14465  cnmpt21  14470  cnmpt2t  14472  cnmpt22  14473  psmetxrge0  14511  xmeterval  14614  comet  14678  txmetcnp  14697  qtopbasss  14700  cnmetdval  14708  remetdval  14726  tgqioo  14734  mpomulcn  14745