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

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

Proof of Theorem fofn
StepHypRef Expression
1 fof 6820 . 2 (𝐹:𝐴onto𝐵𝐹:𝐴𝐵)
21ffnd 6737 1 (𝐹:𝐴onto𝐵𝐹 Fn 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   Fn wfn 6556  ontowfo 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