| Metamath Proof Explorer |
< Previous
Next >
Related theorems Unicode version |
| Description: Define a function (mapping) with domain and codomain. Definition 6.15(3) of [TakeutiZaring] p. 27. For alternate definitions, see dff2 4918, dff3 4919, and dff4 4920. |
| Ref | Expression |
|---|---|
| df-f |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cA |
. . 3
| |
| 2 | cB |
. . 3
| |
| 3 | cF |
. . 3
| |
| 4 | 1, 2, 3 | wf 4159 |
. 2
|
| 5 | 3, 1 | wfn 4158 |
. . 3
|
| 6 | 3 | crn 4152 |
. . . 4
|
| 7 | 6, 2 | wss 2859 |
. . 3
|
| 8 | 5, 7 | wa 433 |
. 2
|
| 9 | 4, 8 | wb 231 |
1
|
| Colors of variables: wff set class |
| This definition is referenced by: feq1 4685 feq2 4686 feq3 4687 hbf 4696 ffn 4698 dffn2 4699 frn 4704 dffn3 4705 fss 4706 fco 4707 funssxp 4709 fun 4712 fnfco 4713 fssres 4714 fcoi2 4717 fint 4721 fin 4722 f0 4727 fconst 4729 fof 4744 dff1o2 4766 ffoss 4790 dff2 4918 dff3 4919 fopab2 4927 ffnfv 4932 fopabco 4936 fpr 4943 dff1o6 4987 fmpt2d 5157 1stcof 5186 smores 5303 smores2 5305 iordsmo 5308 mapval2 5598 map0e 5605 sbthlem9 5727 sucdom2 5854 inf3lem6 6000 alephsmo 6291 alephsing 6358 axdc3lem2 6377 ac5b 6394 om2uzf1oi 8197 seq1f 8225 seq1f2 8226 ser1f 8232 reeff1o 9207 ruclem13 9321 infmap2lem2 9379 idcn 10058 lmsslem 10246 ssga 10476 hhssnv 11759 pjfi 12274 nqerf 14533 fresin 14717 elno2 14907 elno3 14908 axdenselem6 14940 dff1o6f 15389 2ndcof 15463 fopab2g 15480 domrancur1b 15548 isppm 15711 homcard 15911 cmptdst 15978 trnij 16068 cnsubsp 16511 cnsubsp2 16512 tailmap 16721 filnet 16730 cnimass 16973 heiborlem29 17068 heiborlem33 17072 pcocn 17161 smoresOLD 17529 iordsmoOLD 17531 |