![]() |
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 6353 | . 2 ⊢ (𝐹:𝐴–onto→𝐵 → 𝐹:𝐴⟶𝐵) | |
2 | 1 | ffund 6282 | 1 ⊢ (𝐹:𝐴–onto→𝐵 → Fun 𝐹) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 Fun wfun 6117 –onto→wfo 6121 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1894 ax-4 1908 ax-5 2009 ax-6 2075 ax-7 2112 ax-9 2173 ax-10 2192 ax-11 2207 ax-12 2220 ax-ext 2803 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 879 df-tru 1660 df-ex 1879 df-nf 1883 df-sb 2068 df-clab 2812 df-cleq 2818 df-clel 2821 df-in 3805 df-ss 3812 df-fn 6126 df-f 6127 df-fo 6129 |
This theorem is referenced by: foimacnv 6395 resdif 6398 fococnv2 6403 fornex 7397 fodomfi2 9196 fin1a2lem7 9543 brdom3 9665 1stf1 17185 1stf2 17186 2ndf1 17188 2ndf2 17189 1stfcl 17190 2ndfcl 17191 qtopcld 21887 qtopcmap 21893 elfm3 22124 bcthlem4 23495 uniiccdif 23744 grporn 27920 xppreima 29987 qtophaus 30437 bdayimaon 32371 nosupno 32377 bdayfun 32416 poimirlem26 33972 poimirlem27 33973 ovoliunnfl 33988 voliunnfl 33990 |
Copyright terms: Public domain | W3C validator |