![]() |
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 6196, dffn3 6203, dffn4 6270, and dffn5 6391. (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 6032 | . 2 wff 𝐴 Fn 𝐵 |
4 | 1 | wfun 6031 | . . 3 wff Fun 𝐴 |
5 | 1 | cdm 5254 | . . . 4 class dom 𝐴 |
6 | 5, 2 | wceq 1620 | . . 3 wff dom 𝐴 = 𝐵 |
7 | 4, 6 | wa 383 | . 2 wff (Fun 𝐴 ∧ dom 𝐴 = 𝐵) |
8 | 3, 7 | wb 196 | 1 wff (𝐴 Fn 𝐵 ↔ (Fun 𝐴 ∧ dom 𝐴 = 𝐵)) |
Colors of variables: wff setvar class |
This definition is referenced by: funfn 6067 fnsng 6087 fnprg 6096 fntpg 6097 fntp 6098 fncnv 6111 fneq1 6128 fneq2 6129 nffn 6136 fnfun 6137 fndm 6139 fnun 6146 fnco 6148 fnssresb 6152 fnres 6156 fnresi 6157 fn0 6160 mptfnf 6164 fnopabg 6166 sbcfng 6191 fdmrn 6213 fcoi1 6227 f00 6236 f1cnvcnv 6258 fores 6273 dff1o4 6294 foimacnv 6303 funfv 6415 fvimacnvALT 6487 respreima 6495 dff3 6523 fpr 6572 fnsnb 6584 fnprb 6624 fnex 6633 fliftf 6716 fnoprabg 6914 fun11iun 7279 f1oweALT 7305 curry1 7425 curry2 7428 tposfn2 7531 wfrlem13 7584 wfr1 7590 tfrlem10 7640 tfr1 7650 frfnom 7687 undifixp 8098 sbthlem9 8231 fodomr 8264 rankf 8818 cardf2 8930 axdc3lem2 9436 nqerf 9915 axaddf 10129 axmulf 10130 uzrdgfni 12922 hashkf 13284 shftfn 13983 imasaddfnlem 16361 imasvscafn 16370 fntopon 20901 cnextf 22042 ftc1cn 23976 grporn 27655 ffsrn 29784 measdivcstOLD 30567 bnj1422 31186 nofnbday 32082 elno2 32084 scutf 32196 fnsingle 32303 fnimage 32313 imageval 32314 dfrecs2 32334 dfrdg4 32335 ftc1cnnc 33766 fnresfnco 41681 funcoressn 41682 afvco2 41731 |
Copyright terms: Public domain | W3C validator |