New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE 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 SF, 5-Jan-2015.) |
Ref | Expression |
---|---|
df-mpt |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vx | . . 3 | |
2 | cA | . . 3 | |
3 | cB | . . 3 | |
4 | 1, 2, 3 | cmpt 5652 | . 2 |
5 | 1 | cv 1641 | . . . . 5 |
6 | 5, 2 | wcel 1710 | . . . 4 |
7 | vy | . . . . . 6 | |
8 | 7 | cv 1641 | . . . . 5 |
9 | 8, 3 | wceq 1642 | . . . 4 |
10 | 6, 9 | wa 358 | . . 3 |
11 | 10, 1, 7 | copab 4623 | . 2 |
12 | 4, 11 | wceq 1642 | 1 |
Colors of variables: wff setvar class |
This definition is referenced by: mpteq12f 5656 nfmpt 5672 nfmpt1 5673 cbvmpt 5677 fconstmpt 5682 mptpreima 5683 dmmpt 5684 dmmptss 5686 rnmpt 5687 funmpt 5688 mptfng 5689 resmpt 5697 fvmptg 5699 dffn5v 5707 mpt2mptx 5709 mptv 5719 mptresid 5721 f1od 5727 releqmpt 5809 enmap2lem1 6064 enmap1lem1 6070 scancan 6332 |
Copyright terms: Public domain | W3C validator |