Theorem fofn 4619

Description: An onto mapping is a function on its domain.

Assertion

Ref	Expression
fofn	|- (F:A-onto->B -> F Fn A)

Proof of Theorem fofn

Step	Hyp	Ref	Expression
1		fof 4617	. 2 |- (F:A-onto->B -> F:A-->B)
2		ffn 4562	. 2 |- (F:A-->B -> F Fn A)
3	1, 2	syl 12	1 |- (F:A-onto->B -> F Fn A)

Syntax hints:   -> wi 3   Fn wfn 3993  -->wf 3994  -onto->wfo 3996

This theorem is referenced by:  fodmrnu 4626  fo00 4669  1stcof 5040  df1st2 5068  df2nd2 5069  1stconst 5070  2ndconst 5071  fparlem1 5081  fparlem2 5082  fsplit 5086  ac6sfilem2 5507  ac6sfi 5509  fodomfi 5656  infmap2lem2 8849  grprn 9336  subgres 9426  gapm 9462  vcoprnelem 9529  0vfval 9557  upxp 10225  uptx 10226  txcnopab 10228  2txcn 10229  elfilmap3 10314  cncomp 10331  cayleylem3 13643  prj1 14395  imfstnrelc 14396  surjsec2 14467  topgrpsubcnlem 14981  trhom 14983  filnetlem5 15644  filnet 15645  cnoprab1 15921  cnoprab2 15922  heiborlem33 15987

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-10 1308  ax-12 1310  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-an 242  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877  df-clel 1880  df-in 2603  df-ss 2605  df-f 4010  df-fo 4012

Copyright terms: Public domain