| 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 6738, dffn3 6748, dffn4 6826, and dffn5 6967. (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 6556 | . 2 wff 𝐴 Fn 𝐵 |
| 4 | 1 | wfun 6555 | . . 3 wff Fun 𝐴 |
| 5 | 1 | cdm 5685 | . . . 4 class dom 𝐴 |
| 6 | 5, 2 | wceq 1540 | . . 3 wff dom 𝐴 = 𝐵 |
| 7 | 4, 6 | wa 395 | . 2 wff (Fun 𝐴 ∧ dom 𝐴 = 𝐵) |
| 8 | 3, 7 | wb 206 | 1 wff (𝐴 Fn 𝐵 ↔ (Fun 𝐴 ∧ dom 𝐴 = 𝐵)) |
| Colors of variables: wff setvar class |
| This definition is referenced by: funfn 6596 fnsng 6618 fnprg 6625 fntpg 6626 fntp 6627 fncnv 6639 fneq1 6659 fneq2 6660 nffn 6667 fnfun 6668 fndm 6671 fnun 6682 fnssresb 6690 fnres 6695 idfn 6696 fn0 6699 mptfnf 6703 fnopabg 6705 sbcfng 6733 fdmrn 6767 fcoi1 6782 f00 6790 f1cnvcnv 6813 fores 6830 dff1o4 6856 foimacnv 6865 funfv 6996 fvimacnvALT 7077 respreima 7086 dff3 7120 fpr 7174 fnsnb 7186 fnprb 7228 fnex 7237 fliftf 7335 fnoprabg 7556 fiun 7967 f1iun 7968 f1oweALT 7997 curry1 8129 curry2 8132 tposfn2 8273 frrlem11 8321 frrlem12 8322 fpr1 8328 wfrlem13OLD 8361 wfr1OLD 8367 tfrlem10 8427 tfr1 8437 frfnom 8475 undifixp 8974 sbthlem9 9131 fodomr 9168 fodomfir 9368 frr1 9799 rankf 9834 cardf2 9983 axdc3lem2 10491 nqerf 10970 axaddf 11185 axmulf 11186 uzrdgfni 13999 hashkf 14371 shftfn 15112 imasaddfnlem 17573 imasvscafn 17582 fntopon 22930 cnextf 24074 ftc1cn 26084 nofnbday 27697 scutf 27857 noseqrdgfn 28312 grporn 30540 ffsrn 32740 measdivcstALTV 34226 bnj1422 34851 satff 35415 fnsingle 35920 fnimage 35930 imageval 35931 dfrecs2 35951 dfrdg4 35952 bj-isrvec 37295 ftc1cnnc 37699 modelaxreplem1 44995 fnresfnco 47053 funcoressn 47054 afvco2 47188 |
| Copyright terms: Public domain | W3C validator |