Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > df-mpt | Unicode version |
Description: Define maps-to notation for defining a function via a rule. Read as "the function defined by the map from (in ) to ." The class expression is the value of the function at and normally contains the variable . Similar to the definition of mapping in [ChoquetDD] p. 2. (Contributed by NM, 17-Feb-2008.) |
Ref | Expression |
---|---|
df-mpt |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vx | . . 3 | |
2 | cA | . . 3 | |
3 | cB | . . 3 | |
4 | 1, 2, 3 | cmpt 4037 | . 2 |
5 | 1 | cv 1341 | . . . . 5 |
6 | 5, 2 | wcel 2135 | . . . 4 |
7 | vy | . . . . . 6 | |
8 | 7 | cv 1341 | . . . . 5 |
9 | 8, 3 | wceq 1342 | . . . 4 |
10 | 6, 9 | wa 103 | . . 3 |
11 | 10, 1, 7 | copab 4036 | . 2 |
12 | 4, 11 | wceq 1342 | 1 |
Colors of variables: wff set class |
This definition is referenced by: mpteq12f 4056 nfmpt 4068 nfmpt1 4069 cbvmptf 4070 cbvmpt 4071 mptv 4073 fconstmpt 4645 mptrel 4726 rnmpt 4846 resmpt 4926 mptresid 4932 mptcnv 5000 mptpreima 5091 funmpt 5220 dfmpt3 5304 mptfng 5307 mptun 5313 dffn5im 5526 fvmptss2 5555 fvmptg 5556 fndmin 5586 f1ompt 5630 fmptco 5645 mpomptx 5924 f1ocnvd 6034 f1od2 6194 dftpos4 6222 mapsncnv 6652 |
Copyright terms: Public domain | W3C validator |