![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > fofun | Structured version Visualization version GIF version |
Description: An onto mapping is a function. (Contributed by NM, 29-Mar-2008.) |
Ref | Expression |
---|---|
fofun | ⊢ (𝐹:𝐴–onto→𝐵 → Fun 𝐹) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fof 6805 | . 2 ⊢ (𝐹:𝐴–onto→𝐵 → 𝐹:𝐴⟶𝐵) | |
2 | 1 | ffund 6720 | 1 ⊢ (𝐹:𝐴–onto→𝐵 → Fun 𝐹) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 Fun wfun 6536 –onto→wfo 6540 |
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 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2698 |
This theorem depends on definitions: df-bi 206 df-an 396 df-tru 1537 df-ex 1775 df-sb 2061 df-clab 2705 df-cleq 2719 df-clel 2805 df-v 3471 df-in 3951 df-ss 3961 df-fn 6545 df-f 6546 df-fo 6548 |
This theorem is referenced by: foco 6819 foimacnv 6850 resdif 6854 fococnv2 6859 focdmex 7953 fodomfi2 10075 fin1a2lem7 10421 brdom3 10543 1stf1 18174 1stf2 18175 2ndf1 18177 2ndf2 18178 1stfcl 18179 2ndfcl 18180 qtopcld 23604 qtopcmap 23610 elfm3 23841 bcthlem4 25242 uniiccdif 25494 bdayimaon 27613 nosupno 27623 noinfno 27638 bdayfun 27692 noeta2 27704 precsexlem10 28101 precsexlem11 28102 grporn 30318 xppreima 32415 fsuppcurry1 32491 fsuppcurry2 32492 qtophaus 33373 poimirlem26 37054 poimirlem27 37055 ovoliunnfl 37070 voliunnfl 37072 |
Copyright terms: Public domain | W3C validator |