![]() |
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 6295, dffn3 6304, dffn4 6374, and dffn5 6503. (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 6132 | . 2 wff 𝐴 Fn 𝐵 |
4 | 1 | wfun 6131 | . . 3 wff Fun 𝐴 |
5 | 1 | cdm 5357 | . . . 4 class dom 𝐴 |
6 | 5, 2 | wceq 1601 | . . 3 wff dom 𝐴 = 𝐵 |
7 | 4, 6 | wa 386 | . 2 wff (Fun 𝐴 ∧ dom 𝐴 = 𝐵) |
8 | 3, 7 | wb 198 | 1 wff (𝐴 Fn 𝐵 ↔ (Fun 𝐴 ∧ dom 𝐴 = 𝐵)) |
Colors of variables: wff setvar class |
This definition is referenced by: funfn 6167 fnsng 6188 fnprg 6195 fntpg 6196 fntp 6197 fncnv 6209 fneq1 6226 fneq2 6227 nffn 6234 fnfun 6235 fndm 6237 fnun 6245 fnco 6247 fnssresb 6251 fnres 6255 fnresi 6256 fn0 6259 mptfnf 6263 fnopabg 6265 sbcfng 6290 fdmrn 6316 fcoi1 6330 f00 6339 f1cnvcnv 6362 fores 6378 dff1o4 6401 foimacnv 6410 funfv 6527 fvimacnvALT 6601 respreima 6610 dff3 6638 fpr 6689 fnsnb 6701 fnprb 6746 fnex 6755 fliftf 6839 fnoprabg 7040 fun11iun 7407 f1oweALT 7431 curry1 7552 curry2 7555 tposfn2 7658 wfrlem13 7712 wfr1 7718 tfrlem10 7768 tfr1 7778 frfnom 7815 undifixp 8232 sbthlem9 8368 fodomr 8401 rankf 8956 cardf2 9104 axdc3lem2 9610 nqerf 10089 axaddf 10304 axmulf 10305 uzrdgfni 13081 hashkf 13443 shftfn 14226 imasaddfnlem 16585 imasvscafn 16594 fntopon 21147 cnextf 22289 ftc1cn 24254 grporn 27965 ffsrn 30087 measdivcstOLD 30893 bnj1422 31515 nofnbday 32402 elno2 32404 scutf 32516 fnsingle 32623 fnimage 32633 imageval 32634 dfrecs2 32654 dfrdg4 32655 ftc1cnnc 34118 fnresfnco 42119 funcoressn 42120 afvco2 42231 |
Copyright terms: Public domain | W3C validator |