Metamath Proof Explorer


Definition df-fv

Description: Define the value of a function, ( FA ) , also known as function application. For example, ( cos0 ) = 1 (we prove this in cos0 after we define cosine in df-cos ). Typically, function F is defined using maps-to notation (see df-mpt and df-mpo ), but this is not required. For example, F = { <. 2 , 6 >. , <. 3 , 9 >. } -> ( F3 ) = 9 ( ex-fv ). Note that df-ov will define two-argument functions using ordered pairs as ( A F B ) = ( F<. A , B >. ) . This particular definition is quite convenient: it can be applied to any class and evaluates to the empty set when it is not meaningful (as shown by ndmfv and fvprc ). 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 F ( A ) notation for a function's value at A , i.e., " F of A ", but without context-dependent notational ambiguity. Alternate definitions are dffv2 , dffv3 , fv2 , and fv3 (the latter two previously required A to be a set.) Restricted equivalents that require F to be a function are shown in funfv and funfv2 . For the familiar definition of function value in terms of ordered pair membership, see funopfvb . (Contributed by NM, 1-Aug-1994) Revised to use iota . Original version is now Theorem dffv4 . (Revised by Scott Fenton, 6-Oct-2017)

Ref Expression
Assertion df-fv ( 𝐹𝐴 ) = ( ℩ 𝑥 𝐴 𝐹 𝑥 )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cF 𝐹
1 cA 𝐴
2 1 0 cfv ( 𝐹𝐴 )
3 vx 𝑥
4 3 cv 𝑥
5 1 4 0 wbr 𝐴 𝐹 𝑥
6 5 3 cio ( ℩ 𝑥 𝐴 𝐹 𝑥 )
7 2 6 wceq ( 𝐹𝐴 ) = ( ℩ 𝑥 𝐴 𝐹 𝑥 )