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 3989 | . 2 |
5 | 1 | cv 1330 | . . . . 5 |
6 | 5, 2 | wcel 1480 | . . . 4 |
7 | vy | . . . . . 6 | |
8 | 7 | cv 1330 | . . . . 5 |
9 | 8, 3 | wceq 1331 | . . . 4 |
10 | 6, 9 | wa 103 | . . 3 |
11 | 10, 1, 7 | copab 3988 | . 2 |
12 | 4, 11 | wceq 1331 | 1 |
Colors of variables: wff set class |
This definition is referenced by: mpteq12f 4008 nfmpt 4020 nfmpt1 4021 cbvmptf 4022 cbvmpt 4023 mptv 4025 fconstmpt 4586 mptrel 4667 rnmpt 4787 resmpt 4867 mptresid 4873 mptcnv 4941 mptpreima 5032 funmpt 5161 dfmpt3 5245 mptfng 5248 mptun 5254 dffn5im 5467 fvmptss2 5496 fvmptg 5497 fndmin 5527 f1ompt 5571 fmptco 5586 mpomptx 5862 f1ocnvd 5972 f1od2 6132 dftpos4 6160 mapsncnv 6589 |
Copyright terms: Public domain | W3C validator |