| 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 6820 | . 2 ⊢ (𝐹:𝐴–onto→𝐵 → 𝐹:𝐴⟶𝐵) | |
| 2 | 1 | ffnd 6737 | 1 ⊢ (𝐹:𝐴–onto→𝐵 → 𝐹 Fn 𝐴) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 Fn wfn 6556 –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-f 6565 df-fo 6567 |
| This theorem is referenced by: fodmrnu 6828 foun 6866 fo00 6884 foelcdmi 6970 cbvfo 7309 foeqcnvco 7320 canth 7385 br1steqg 8036 br2ndeqg 8037 1stcof 8044 2ndcof 8045 df1st2 8123 df2nd2 8124 1stconst 8125 2ndconst 8126 fsplit 8142 smoiso2 8409 fodomfi 9350 fodomfiOLD 9370 brwdom2 9613 fodomfi2 10100 fpwwe 10686 imasaddfnlem 17573 imasvscafn 17582 imasleval 17586 dmaf 18094 cdaf 18095 imasmnd2 18787 imasgrp2 19073 efgrelexlemb 19768 efgredeu 19770 imasrng 20174 imasring 20327 znf1o 21570 zzngim 21571 indlcim 21860 1stcfb 23453 upxp 23631 uptx 23633 cnmpt1st 23676 cnmpt2nd 23677 qtoptopon 23712 qtopcld 23721 qtopeu 23724 qtoprest 23725 imastopn 23728 qtophmeo 23825 elfm3 23958 uniiccdif 25613 dirith 27573 nosupno 27748 nosupbday 27750 noinfno 27763 noinfbday 27765 noetasuplem4 27781 noetainflem4 27785 bdayfn 27818 grporn 30540 0vfval 30625 foresf1o 32523 2ndimaxp 32656 2ndresdju 32659 xppreima2 32661 1stpreimas 32715 1stpreima 32716 2ndpreima 32717 fsuppcurry1 32736 fsuppcurry2 32737 ffsrn 32740 gsummpt2d 33052 qusker 33377 imaslmod 33381 qtopt1 33834 qtophaus 33835 circcn 33837 cnre2csqima 33910 sigapildsys 34163 carsgclctunlem3 34322 fnbigcup 35902 filnetlem4 36382 ovoliunnfl 37669 voliunnfl 37671 volsupnfl 37672 ssnnf1octb 45199 nnfoctbdj 46471 fcoreslem4 47078 fcoresf1 47081 fargshiftfo 47429 |
| Copyright terms: Public domain | W3C validator |