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 4050 | . 2 |
5 | 1 | cv 1347 | . . . . 5 |
6 | 5, 2 | wcel 2141 | . . . 4 |
7 | vy | . . . . . 6 | |
8 | 7 | cv 1347 | . . . . 5 |
9 | 8, 3 | wceq 1348 | . . . 4 |
10 | 6, 9 | wa 103 | . . 3 |
11 | 10, 1, 7 | copab 4049 | . 2 |
12 | 4, 11 | wceq 1348 | 1 |
Colors of variables: wff set class |
This definition is referenced by: mpteq12f 4069 nfmpt 4081 nfmpt1 4082 cbvmptf 4083 cbvmpt 4084 mptv 4086 fconstmpt 4658 mptrel 4739 rnmpt 4859 resmpt 4939 mptresid 4945 mptcnv 5013 mptpreima 5104 funmpt 5236 dfmpt3 5320 mptfng 5323 mptun 5329 dffn5im 5542 fvmptss2 5571 fvmptg 5572 fndmin 5603 f1ompt 5647 fmptco 5662 mpomptx 5944 f1ocnvd 6051 f1od2 6214 dftpos4 6242 mapsncnv 6673 |
Copyright terms: Public domain | W3C validator |