Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-fv Structured version   Unicode version

Definition df-fv 4853
 Description: Define the value of a function, , also known as function application. For example, . Typically, function is defined using maps-to notation (see df-mpt 3811), but this is not required. For example, F = { 2 , 6 , 3 , 9 } -> ( F 3 ) = 9 . We will later define two-argument functions using ordered pairs as . This particular definition is quite convenient: it can be applied to any class and evaluates to the empty set when it is not meaningful. The left apostrophe notation originated with Peano and was adopted in Definition *30.01 of [WhiteheadRussell] p. 235, Definition 10.11 of [Quine] p. 68, and Definition 6.11 of [TakeutiZaring] p. 26. It means the same thing as the more familiar notation for a function's value at , i.e. " of ," but without context-dependent notational ambiguity. (Contributed by NM, 1-Aug-1994.) Revised to use . (Revised by Scott Fenton, 6-Oct-2017.)
Assertion
Ref Expression
df-fv
Distinct variable groups:   ,   ,

Detailed syntax breakdown of Definition df-fv
StepHypRef Expression
1 cA . . 3
2 cF . . 3
31, 2cfv 4845 . 2
4 vx . . . . 5
54cv 1241 . . . 4
61, 5, 2wbr 3755 . . 3
76, 4cio 4808 . 2
83, 7wceq 1242 1
 Colors of variables: wff set class This definition is referenced by:  tz6.12-2  5112  fveu  5113  fv2  5116  dffv3g  5117  fveq1  5120  fveq2  5121  nffv  5128  fvss  5132  funfvex  5135  fvres  5141  tz6.12-1  5143  nfvres  5149  0fv  5151  csbfv12g  5152  ovtposg  5815
 Copyright terms: Public domain W3C validator