![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > funfnd | Structured version Visualization version GIF version |
Description: A function is a function on its domain. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
Ref | Expression |
---|---|
funfnd.1 | ⊢ (𝜑 → Fun 𝐴) |
Ref | Expression |
---|---|
funfnd | ⊢ (𝜑 → 𝐴 Fn dom 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | funfnd.1 | . 2 ⊢ (𝜑 → Fun 𝐴) | |
2 | funfn 6529 | . 2 ⊢ (Fun 𝐴 ↔ 𝐴 Fn dom 𝐴) | |
3 | 1, 2 | sylib 217 | 1 ⊢ (𝜑 → 𝐴 Fn dom 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 dom cdm 5632 Fun wfun 6488 Fn wfn 6489 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-9 2116 ax-ext 2707 |
This theorem depends on definitions: df-bi 206 df-an 397 df-ex 1782 df-cleq 2728 df-fn 6497 |
This theorem is referenced by: fncofn 6615 resfunexg 7162 funiunfv 7192 funelss 7976 funsssuppss 8118 frrlem4 8217 wfrlem4OLD 8255 smores2 8297 tfrlem1 8319 resfnfinfin 9273 resfifsupp 9330 ordtypelem4 9454 ordtypelem9 9459 ordtypelem10 9460 brdom3 10461 brdom5 10462 brdom4 10463 fpwwe2lem10 10573 hashimarn 14337 resunimafz0 14339 isstruct2 17018 invf 17648 lindfrn 21223 ofco2 21796 dfac14 22965 perfdvf 25263 c1lip2 25358 taylf 25716 elno2 26998 noinfbnd2lem1 27074 noetainflem4 27084 lpvtx 27917 upgrle2 27954 uhgrvtxedgiedgb 27985 uhgr2edg 28054 ushgredgedg 28075 ushgredgedgloop 28077 subgruhgredgd 28130 subuhgr 28132 subupgr 28133 subumgr 28134 subusgr 28135 upgrres 28152 umgrres 28153 vtxdun 28327 upgrewlkle2 28452 eupthvdres 29077 cycpmfvlem 31856 cycpmfv3 31859 sitgf 32838 cardpred 33585 nummin 33586 bj-gabima 35399 gneispace 42386 gneispacef2 42388 funimaeq 43448 limsupresxr 43977 liminfresxr 43978 funcoressn 45246 |
Copyright terms: Public domain | W3C validator |