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

Theorem fofn 6030
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 6028 . 2 (𝐹:𝐴onto𝐵𝐹:𝐴𝐵)
2 ffn 5958 . 2 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
31, 2syl 17 1 (𝐹:𝐴onto𝐵𝐹 Fn 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   Fn wfn 5799  wf 5800  ontowfo 5802
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-in 3547  df-ss 3554  df-f 5808  df-fo 5810
This theorem is referenced by:  fodmrnu  6036  foun  6068  fo00  6084  foelrni  6154  cbvfo  6444  foeqcnvco  6455  canth  6508  1stcof  7087  2ndcof  7088  df1st2  7150  df2nd2  7151  1stconst  7152  2ndconst  7153  fsplit  7169  smoiso2  7353  fodomfi  8124  brwdom2  8361  fodomfi2  8766  fpwwe  9347  imasaddfnlem  16011  imasvscafn  16020  imasleval  16024  dmaf  16522  cdaf  16523  imasmnd2  17150  imasgrp2  17353  efgrelexlemb  17986  efgredeu  17988  imasring  18442  znf1o  19719  zzngim  19720  indlcim  19998  1stcfb  21058  upxp  21236  uptx  21238  cnmpt1st  21281  cnmpt2nd  21282  qtoptopon  21317  qtopcld  21326  qtopeu  21329  qtoprest  21330  imastopn  21333  qtophmeo  21430  elfm3  21564  uniiccdif  23152  dirith  25018  fargshiftfo  26166  grporn  26759  0vfval  26845  foresf1o  28727  xppreima2  28830  1stpreimas  28866  1stpreima  28867  2ndpreima  28868  ffsrn  28892  gsummpt2d  29112  qtopt1  29230  qtophaus  29231  circcn  29233  cnre2csqima  29285  sigapildsys  29552  carsgclctunlem3  29709  br1steq  30917  br2ndeq  30918  fnbigcup  31178  filnetlem4  31546  ovoliunnfl  32621  voliunnfl  32623  volsupnfl  32624  ssnnf1octb  38377  nnfoctbdj  39349
  Copyright terms: Public domain W3C validator