![]() |
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 over 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 6165 | . 2 ⊢ (Fun 𝐴 ↔ 𝐴 Fn dom 𝐴) | |
3 | 1, 2 | sylib 210 | 1 ⊢ (𝜑 → 𝐴 Fn dom 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 dom cdm 5355 Fun wfun 6129 Fn wfn 6130 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-9 2116 ax-ext 2754 |
This theorem depends on definitions: df-bi 199 df-an 387 df-ex 1824 df-cleq 2770 df-fn 6138 |
This theorem is referenced by: resfunexg 6751 funiunfv 6778 funsssuppss 7603 wfrlem4 7700 smores2 7734 tfrlem1 7755 resfnfinfin 8534 resfifsupp 8591 ordtypelem4 8715 ordtypelem9 8720 ordtypelem10 8721 brdom3 9685 brdom5 9686 brdom4 9687 fpwwe2lem11 9797 hashimarn 13541 resunimafz0 13543 isstruct2 16265 invf 16813 uhgrvtxedgiedgb 26484 ushgredgedgloop 26577 upgrres 26653 umgrres 26654 funimaeq 40372 limsupresxr 40906 liminfresxr 40907 |
Copyright terms: Public domain | W3C validator |