MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fofn Unicode version

Theorem fofn 5802
Description: An onto mapping is a function on its domain. (Contributed by NM, 16-Dec-2008.)
Assertion
Ref Expression
fofn

Proof of Theorem fofn
StepHypRef Expression
1 fof 5800 . 2
2 ffn 5736 . 2
31, 2syl 16 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  Fnwfn 5588  -->wf 5589  -onto->wfo 5591
This theorem is referenced by:  fodmrnu  5808  foun  5839  fo00  5854  foelrni  5921  cbvfo  6192  foeqcnvco  6203  canth  6254  1stcof  6828  2ndcof  6829  df1st2  6886  df2nd2  6887  1stconst  6888  2ndconst  6889  fsplit  6905  smoiso2  7059  fodomfi  7819  brwdom2  8020  fodomfi2  8462  fpwwe  9045  imasaddfnlem  14925  imasvscafn  14934  imasleval  14938  dmaf  15376  cdaf  15377  imasmnd2  15957  imasgrp2  16185  efgrelexlemb  16768  efgredeu  16770  imasring  17268  znf1o  18590  zzngim  18591  indlcim  18875  1stcfb  19946  upxp  20124  uptx  20126  cnmpt1st  20169  cnmpt2nd  20170  qtoptopon  20205  qtopcld  20214  qtopeu  20217  qtoprest  20218  imastopn  20221  qtophmeo  20318  elfm3  20451  uniiccdif  21987  dirith  23714  fargshiftfo  24638  grporn  25214  subgores  25306  vcoprnelem  25471  0vfval  25499  foresf1o  27403  xppreima2  27488  1stpreima  27524  2ndpreima  27525  ffsrn  27552  qtopt1  27838  qtophaus  27839  circcn  27841  cnre2csqima  27893  br1steq  29204  br2ndeq  29205  fnbigcup  29551  ovoliunnfl  30056  voliunnfl  30058  volsupnfl  30059  filnetlem4  30199
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-in 3482  df-ss 3489  df-f 5597  df-fo 5599
  Copyright terms: Public domain W3C validator