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 6378 | . 2 ⊢ (Fun 𝐴 ↔ 𝐴 Fn dom 𝐴) | |
3 | 1, 2 | sylib 220 | 1 ⊢ (𝜑 → 𝐴 Fn dom 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 dom cdm 5548 Fun wfun 6342 Fn wfn 6343 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1905 ax-6 1964 ax-7 2009 ax-9 2118 ax-ext 2791 |
This theorem depends on definitions: df-bi 209 df-an 399 df-ex 1775 df-cleq 2812 df-fn 6351 |
This theorem is referenced by: resfunexg 6970 funiunfv 6999 funelss 7738 funsssuppss 7848 wfrlem4 7950 smores2 7983 tfrlem1 8004 resfnfinfin 8796 resfifsupp 8853 ordtypelem4 8977 ordtypelem9 8982 ordtypelem10 8983 brdom3 9942 brdom5 9943 brdom4 9944 fpwwe2lem11 10054 hashimarn 13793 resunimafz0 13795 isstruct2 16485 invf 17030 lindfrn 20957 ofco2 21052 dfac14 22218 perfdvf 24493 c1lip2 24587 taylf 24941 lpvtx 26845 upgrle2 26882 uhgrvtxedgiedgb 26913 uhgr2edg 26982 ushgredgedg 27003 ushgredgedgloop 27005 subgruhgredgd 27058 subuhgr 27060 subupgr 27061 subumgr 27062 subusgr 27063 upgrres 27080 umgrres 27081 vtxdun 27255 upgrewlkle2 27380 eupthvdres 28006 cycpmfvlem 30747 cycpmfv3 30750 sitgf 31598 frrlem4 33119 elno2 33154 gneispace 40475 gneispacef2 40477 funimaeq 41508 limsupresxr 42037 liminfresxr 42038 funcoressn 43268 |
Copyright terms: Public domain | W3C validator |