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 6590 | . 2 ⊢ (𝐹:𝐴–onto→𝐵 → 𝐹:𝐴⟶𝐵) | |
2 | 1 | ffnd 6515 | 1 ⊢ (𝐹:𝐴–onto→𝐵 → 𝐹 Fn 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 Fn wfn 6350 –onto→wfo 6353 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2793 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-clab 2800 df-cleq 2814 df-clel 2893 df-in 3943 df-ss 3952 df-f 6359 df-fo 6361 |
This theorem is referenced by: fodmrnu 6598 foun 6633 fo00 6650 foelrni 6727 cbvfo 7045 foeqcnvco 7056 canth 7111 br1steqg 7711 br2ndeqg 7712 1stcof 7719 2ndcof 7720 df1st2 7793 df2nd2 7794 1stconst 7795 2ndconst 7796 fsplit 7812 fsplitOLD 7813 smoiso2 8006 fodomfi 8797 brwdom2 9037 fodomfi2 9486 fpwwe 10068 imasaddfnlem 16801 imasvscafn 16810 imasleval 16814 dmaf 17309 cdaf 17310 imasmnd2 17948 imasgrp2 18214 efgrelexlemb 18876 efgredeu 18878 imasring 19369 znf1o 20698 zzngim 20699 indlcim 20984 1stcfb 22053 upxp 22231 uptx 22233 cnmpt1st 22276 cnmpt2nd 22277 qtoptopon 22312 qtopcld 22321 qtopeu 22324 qtoprest 22325 imastopn 22328 qtophmeo 22425 elfm3 22558 uniiccdif 24179 dirith 26105 grporn 28298 0vfval 28383 foresf1o 30265 xppreima2 30395 1stpreimas 30441 1stpreima 30442 2ndpreima 30443 fsuppcurry1 30461 fsuppcurry2 30462 ffsrn 30465 gsummpt2d 30687 qusker 30918 imaslmod 30922 qtopt1 31099 qtophaus 31100 circcn 31102 cnre2csqima 31154 sigapildsys 31421 carsgclctunlem3 31578 nosupno 33203 nosupbday 33205 noetalem3 33219 bdayfn 33243 fnbigcup 33362 filnetlem4 33729 ovoliunnfl 34949 voliunnfl 34951 volsupnfl 34952 ssnnf1octb 41476 nnfoctbdj 42758 fargshiftfo 43622 |
Copyright terms: Public domain | W3C validator |