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 5960, dffn3 5967, dffn4 6034, and dffn5 6151. (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 5799 | . 2 wff 𝐴 Fn 𝐵 |
4 | 1 | wfun 5798 | . . 3 wff Fun 𝐴 |
5 | 1 | cdm 5038 | . . . 4 class dom 𝐴 |
6 | 5, 2 | wceq 1475 | . . 3 wff dom 𝐴 = 𝐵 |
7 | 4, 6 | wa 383 | . 2 wff (Fun 𝐴 ∧ dom 𝐴 = 𝐵) |
8 | 3, 7 | wb 195 | 1 wff (𝐴 Fn 𝐵 ↔ (Fun 𝐴 ∧ dom 𝐴 = 𝐵)) |
Colors of variables: wff setvar class |
This definition is referenced by: funfn 5833 fnsng 5852 fnprg 5861 fntpg 5862 fntp 5863 fncnv 5876 fneq1 5893 fneq2 5894 nffn 5901 fnfun 5902 fndm 5904 fnun 5911 fnco 5913 fnssresb 5917 fnres 5921 fnresi 5922 fn0 5924 mptfnf 5928 fnopabg 5930 sbcfng 5955 fdmrn 5977 fcoi1 5991 f00 6000 f1cnvcnv 6022 fores 6037 dff1o4 6058 foimacnv 6067 funfv 6175 fvimacnvALT 6244 respreima 6252 dff3 6280 fpr 6326 fnsnb 6337 fnprb 6377 fnex 6386 fliftf 6465 fnoprabg 6659 fun11iun 7019 f1oweALT 7043 curry1 7156 curry2 7159 tposfn2 7261 wfrlem13 7314 wfr1 7320 tfrlem10 7370 tfr1 7380 frfnom 7417 undifixp 7830 sbthlem9 7963 fodomr 7996 rankf 8540 cardf2 8652 axdc3lem2 9156 nqerf 9631 axaddf 9845 axmulf 9846 uzrdgfni 12619 hashkf 12981 shftfn 13661 imasaddfnlem 16011 imasvscafn 16020 cnextf 21680 ftc1cn 23610 grporn 26759 ffsrn 28892 measdivcstOLD 29614 bnj145OLD 30049 bnj1422 30162 nofnbday 31049 elno2 31051 bdayfn 31078 fnsingle 31196 fnimage 31206 imageval 31207 dfrecs2 31227 dfrdg4 31228 bj-fntopon 32243 ftc1cnnc 32654 fnresfnco 39855 funcoressn 39856 afvco2 39905 |
Copyright terms: Public domain | W3C validator |