![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > df-fn | Structured version Visualization version GIF version |
Description: Define a function with domain. Definition 6.15(1) of [TakeutiZaring] p. 27. For alternate definitions, see dffn2 6730, dffn3 6740, dffn4 6821, and dffn5 6961. (Contributed by NM, 1-Aug-1994.) |
Ref | Expression |
---|---|
df-fn | ⊢ (𝐴 Fn 𝐵 ↔ (Fun 𝐴 ∧ dom 𝐴 = 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 class 𝐴 | |
2 | cB | . . 3 class 𝐵 | |
3 | 1, 2 | wfn 6549 | . 2 wff 𝐴 Fn 𝐵 |
4 | 1 | wfun 6548 | . . 3 wff Fun 𝐴 |
5 | 1 | cdm 5682 | . . . 4 class dom 𝐴 |
6 | 5, 2 | wceq 1534 | . . 3 wff dom 𝐴 = 𝐵 |
7 | 4, 6 | wa 394 | . 2 wff (Fun 𝐴 ∧ dom 𝐴 = 𝐵) |
8 | 3, 7 | wb 205 | 1 wff (𝐴 Fn 𝐵 ↔ (Fun 𝐴 ∧ dom 𝐴 = 𝐵)) |
Colors of variables: wff setvar class |
This definition is referenced by: funfn 6589 fnsng 6611 fnprg 6618 fntpg 6619 fntp 6620 fncnv 6632 fneq1 6651 fneq2 6652 nffn 6659 fnfun 6660 fndm 6663 fnun 6674 fncoOLD 6679 fnssresb 6683 fnres 6688 idfn 6689 fn0 6692 mptfnf 6696 fnopabg 6698 sbcfng 6725 fdmrn 6760 fcoi1 6776 f00 6784 f1cnvcnv 6807 fores 6825 dff1o4 6851 foimacnv 6860 funfv 6989 fvimacnvALT 7070 respreima 7079 dff3 7114 fpr 7168 fnsnb 7180 fnprb 7225 fnex 7234 fliftf 7327 fnoprabg 7548 fiun 7956 f1iun 7957 f1oweALT 7986 curry1 8118 curry2 8121 tposfn2 8263 frrlem11 8311 frrlem12 8312 fpr1 8318 wfrlem13OLD 8351 wfr1OLD 8357 tfrlem10 8417 tfr1 8427 frfnom 8465 undifixp 8963 sbthlem9 9129 fodomr 9166 fodomfir 9370 frr1 9802 rankf 9837 cardf2 9986 axdc3lem2 10494 nqerf 10973 axaddf 11188 axmulf 11189 uzrdgfni 13978 hashkf 14349 shftfn 15078 imasaddfnlem 17543 imasvscafn 17552 fntopon 22917 cnextf 24061 ftc1cn 26069 nofnbday 27682 scutf 27842 noseqrdgfn 28280 grporn 30454 ffsrn 32643 measdivcstALTV 34058 bnj1422 34682 satff 35238 fnsingle 35743 fnimage 35753 imageval 35754 dfrecs2 35774 dfrdg4 35775 bj-isrvec 37001 ftc1cnnc 37393 fnresfnco 46656 funcoressn 46657 afvco2 46789 |
Copyright terms: Public domain | W3C validator |