![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > fofn | Structured version Visualization version GIF version |
Description: An onto mapping is a function on its domain. (Contributed by NM, 16-Dec-2008.) |
Ref | Expression |
---|---|
fofn | ⊢ (𝐹:𝐴–onto→𝐵 → 𝐹 Fn 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fof 6354 | . 2 ⊢ (𝐹:𝐴–onto→𝐵 → 𝐹:𝐴⟶𝐵) | |
2 | 1 | ffnd 6280 | 1 ⊢ (𝐹:𝐴–onto→𝐵 → 𝐹 Fn 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 Fn wfn 6119 –onto→wfo 6122 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1896 ax-4 1910 ax-5 2011 ax-6 2077 ax-7 2114 ax-9 2175 ax-10 2194 ax-11 2209 ax-12 2222 ax-ext 2804 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 881 df-tru 1662 df-ex 1881 df-nf 1885 df-sb 2070 df-clab 2813 df-cleq 2819 df-clel 2822 df-in 3806 df-ss 3813 df-f 6128 df-fo 6130 |
This theorem is referenced by: fodmrnu 6362 foun 6397 fo00 6414 foelrni 6492 cbvfo 6800 foeqcnvco 6811 canth 6864 br1steqg 7451 br2ndeqg 7452 1stcof 7459 2ndcof 7460 df1st2 7528 df2nd2 7529 1stconst 7530 2ndconst 7531 fsplit 7547 smoiso2 7733 fodomfi 8509 brwdom2 8748 fodomfi2 9197 fpwwe 9784 imasaddfnlem 16542 imasvscafn 16551 imasleval 16555 dmaf 17052 cdaf 17053 imasmnd2 17681 imasgrp2 17885 efgrelexlemb 18517 efgredeu 18519 imasring 18974 znf1o 20260 zzngim 20261 indlcim 20547 1stcfb 21620 upxp 21798 uptx 21800 cnmpt1st 21843 cnmpt2nd 21844 qtoptopon 21879 qtopcld 21888 qtopeu 21891 qtoprest 21892 imastopn 21895 qtophmeo 21992 elfm3 22125 uniiccdif 23745 dirith 25632 grporn 27932 0vfval 28017 foresf1o 29892 xppreima2 30000 1stpreimas 30032 1stpreima 30033 2ndpreima 30034 ffsrn 30053 gsummpt2d 30327 qtopt1 30448 qtophaus 30449 circcn 30451 cnre2csqima 30503 sigapildsys 30771 carsgclctunlem3 30928 nosupno 32389 nosupbday 32391 noetalem3 32405 bdayfn 32429 fnbigcup 32548 filnetlem4 32915 ovoliunnfl 33996 voliunnfl 33998 volsupnfl 33999 ssnnf1octb 40191 nnfoctbdj 41465 fargshiftfo 42267 |
Copyright terms: Public domain | W3C validator |