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 6565 | . 2 ⊢ (𝐹:𝐴–onto→𝐵 → 𝐹:𝐴⟶𝐵) | |
2 | 1 | ffund 6491 | 1 ⊢ (𝐹:𝐴–onto→𝐵 → Fun 𝐹) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 Fun wfun 6318 –onto→wfo 6322 |
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 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-ext 2770 |
This theorem depends on definitions: df-bi 210 df-an 400 df-ex 1782 df-sb 2070 df-clab 2777 df-cleq 2791 df-clel 2870 df-v 3443 df-in 3888 df-ss 3898 df-fn 6327 df-f 6328 df-fo 6330 |
This theorem is referenced by: foimacnv 6607 resdif 6610 fococnv2 6615 fornex 7639 fodomfi2 9471 fin1a2lem7 9817 brdom3 9939 1stf1 17434 1stf2 17435 2ndf1 17437 2ndf2 17438 1stfcl 17439 2ndfcl 17440 qtopcld 22318 qtopcmap 22324 elfm3 22555 bcthlem4 23931 uniiccdif 24182 grporn 28304 xppreima 30408 fsuppcurry1 30487 fsuppcurry2 30488 qtophaus 31189 bdayimaon 33310 nosupno 33316 bdayfun 33355 poimirlem26 35083 poimirlem27 35084 ovoliunnfl 35099 voliunnfl 35101 |
Copyright terms: Public domain | W3C validator |