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 6028 | . 2 ⊢ (𝐹:𝐴–onto→𝐵 → 𝐹:𝐴⟶𝐵) | |
2 | ffun 5961 | . 2 ⊢ (𝐹:𝐴⟶𝐵 → Fun 𝐹) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝐹:𝐴–onto→𝐵 → Fun 𝐹) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 Fun wfun 5798 ⟶wf 5800 –onto→wfo 5802 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-in 3547 df-ss 3554 df-fn 5807 df-f 5808 df-fo 5810 |
This theorem is referenced by: foimacnv 6067 resdif 6070 fococnv2 6075 fornex 7028 fodomfi2 8766 fin1a2lem7 9111 brdom3 9231 1stf1 16655 1stf2 16656 2ndf1 16658 2ndf2 16659 1stfcl 16660 2ndfcl 16661 qtopcld 21326 qtopcmap 21332 elfm3 21564 bcthlem4 22932 uniiccdif 23152 grporn 26759 xppreima 28829 qtophaus 29231 bdayfun 31075 poimirlem26 32605 poimirlem27 32606 ovoliunnfl 32621 voliunnfl 32623 |
Copyright terms: Public domain | W3C validator |