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

Theorem fofn 6583
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 6581 . 2 (𝐹:𝐴onto𝐵𝐹:𝐴𝐵)
21ffnd 6504 1 (𝐹:𝐴onto𝐵𝐹 Fn 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   Fn wfn 6338  ontowfo 6341
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-ext 2796
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-v 3482  df-in 3926  df-ss 3936  df-f 6347  df-fo 6349
This theorem is referenced by:  fodmrnu  6589  foun  6624  fo00  6641  foelrni  6718  cbvfo  7037  foeqcnvco  7048  canth  7104  br1steqg  7706  br2ndeqg  7707  1stcof  7714  2ndcof  7715  df1st2  7789  df2nd2  7790  1stconst  7791  2ndconst  7792  fsplit  7808  fsplitOLD  7809  smoiso2  8002  fodomfi  8794  brwdom2  9034  fodomfi2  9484  fpwwe  10066  imasaddfnlem  16801  imasvscafn  16810  imasleval  16814  dmaf  17309  cdaf  17310  imasmnd2  17948  imasgrp2  18214  efgrelexlemb  18876  efgredeu  18878  imasring  19372  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  24185  dirith  26116  grporn  28307  0vfval  28392  foresf1o  30275  xppreima2  30406  1stpreimas  30452  1stpreima  30453  2ndpreima  30454  fsuppcurry1  30472  fsuppcurry2  30473  ffsrn  30476  gsummpt2d  30719  qusker  30951  imaslmod  30955  qtopt1  31159  qtophaus  31160  circcn  31162  cnre2csqima  31211  sigapildsys  31478  carsgclctunlem3  31635  nosupno  33260  nosupbday  33262  noetalem3  33276  bdayfn  33300  fnbigcup  33419  filnetlem4  33786  ovoliunnfl  35044  voliunnfl  35046  volsupnfl  35047  ssnnf1octb  41747  nnfoctbdj  43021  fargshiftfo  43885
  Copyright terms: Public domain W3C validator