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 6510, dffn3 6519, dffn4 6590, and dffn5 6718. (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 6344 | . 2 wff 𝐴 Fn 𝐵 |
4 | 1 | wfun 6343 | . . 3 wff Fun 𝐴 |
5 | 1 | cdm 5549 | . . . 4 class dom 𝐴 |
6 | 5, 2 | wceq 1528 | . . 3 wff dom 𝐴 = 𝐵 |
7 | 4, 6 | wa 396 | . 2 wff (Fun 𝐴 ∧ dom 𝐴 = 𝐵) |
8 | 3, 7 | wb 207 | 1 wff (𝐴 Fn 𝐵 ↔ (Fun 𝐴 ∧ dom 𝐴 = 𝐵)) |
Colors of variables: wff setvar class |
This definition is referenced by: funfn 6379 fnsng 6400 fnprg 6407 fntpg 6408 fntp 6409 fncnv 6421 fneq1 6438 fneq2 6439 nffn 6446 fnfun 6447 fndm 6449 fnun 6457 fnco 6459 fnssresb 6463 fnres 6468 idfn 6469 fnresiOLD 6471 fn0 6473 mptfnf 6477 fnopabg 6479 sbcfng 6505 fdmrn 6532 fcoi1 6546 f00 6555 f1cnvcnv 6578 fores 6594 dff1o4 6617 foimacnv 6626 funfv 6744 fvimacnvALT 6820 respreima 6829 dff3 6859 fpr 6909 fnsnb 6921 fnprb 6963 fnex 6972 fliftf 7057 fnoprabg 7264 fiunw 7632 f1iunw 7633 fiun 7635 f1iun 7636 f1oweALT 7664 curry1 7790 curry2 7793 tposfn2 7905 wfrlem13 7958 wfr1 7964 tfrlem10 8014 tfr1 8024 frfnom 8061 undifixp 8487 sbthlem9 8624 fodomr 8657 rankf 9212 cardf2 9361 axdc3lem2 9862 nqerf 10341 axaddf 10556 axmulf 10557 uzrdgfni 13316 hashkf 13682 shftfn 14422 imasaddfnlem 16791 imasvscafn 16800 fntopon 21462 cnextf 22604 ftc1cn 24569 grporn 28226 ffsrn 30392 measdivcstALTV 31384 bnj1422 32009 satff 32555 frrlem11 33031 frrlem12 33032 fpr1 33037 frr1 33042 nofnbday 33057 scutf 33171 fnsingle 33278 fnimage 33288 imageval 33289 dfrecs2 33309 dfrdg4 33310 ftc1cnnc 34848 fnresfnco 43157 funcoressn 43158 afvco2 43256 |
Copyright terms: Public domain | W3C validator |