| 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 6820 | . 2 ⊢ (𝐹:𝐴–onto→𝐵 → 𝐹:𝐴⟶𝐵) | |
| 2 | 1 | ffund 6740 | 1 ⊢ (𝐹:𝐴–onto→𝐵 → Fun 𝐹) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 Fun wfun 6555 –onto→wfo 6559 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-cleq 2729 df-ss 3968 df-fn 6564 df-f 6565 df-fo 6567 |
| This theorem is referenced by: foco 6834 foimacnv 6865 resdif 6869 fococnv2 6874 focdmex 7980 fodomfi2 10100 fin1a2lem7 10446 brdom3 10568 1stf1 18237 1stf2 18238 2ndf1 18240 2ndf2 18241 1stfcl 18242 2ndfcl 18243 qtopcld 23721 qtopcmap 23727 elfm3 23958 bcthlem4 25361 uniiccdif 25613 bdayimaon 27738 nosupno 27748 noinfno 27763 bdayfun 27817 noeta2 27829 precsexlem10 28240 precsexlem11 28241 grporn 30540 xppreima 32655 fsuppcurry1 32736 fsuppcurry2 32737 qtophaus 33835 poimirlem26 37653 poimirlem27 37654 ovoliunnfl 37669 voliunnfl 37671 |
| Copyright terms: Public domain | W3C validator |