Theorem fof 5547

Description: An onto mapping is a mapping. (Contributed by NM, 3-Aug-1994.)

Assertion

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

Proof of Theorem fof

Step	Hyp	Ref	Expression
1		eqimss 3278	. . 3 |- ( ran F = B -> ran F C_ B )
2	1	anim2i 342	. 2 |- ( ( F Fn A /\ ran F = B ) -> ( F Fn A /\ ran F C_ B ) )
3		df-fo 5323	. 2 |- ( F : A -onto-> B <-> ( F Fn A /\ ran F = B ) )
4		df-f 5321	. 2 |- ( F : A --> B <-> ( F Fn A /\ ran F C_ B ) )
5	2, 3, 4	3imtr4i 201	1 |- ( F : A -onto-> B -> F : A --> B )

Syntax hints:   -> wi 4   /\ wa 104   = wceq 1395   C_ wss 3197   ran crn 4719   Fn wfn 5312   -->wf 5313   -onto->wfo 5315

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-in 3203  df-ss 3210  df-f 5321  df-fo 5323

This theorem is referenced by:  fofun  5548  fofn  5549  dffo2  5551  foima  5552  resdif  5593  ffoss  5603  fconstfvm  5856  cocan2  5911  foeqcnvco  5913  focdmex  6258  algrflem  6373  algrflemg  6374  tposf2  6412  mapsn  6835  ssdomg  6928  fopwdom  6993  fidcenumlemrks  7116  fidcenumlemr  7118  ctmlemr  7271  ctm  7272  ctssdclemn0  7273  ctssdccl  7274  ctssdc  7276  enumctlemm  7277  enumct  7278  fodjuomnilemdc  7307  exmidfodomrlemr  7376  exmidfodomrlemrALT  7377  suplocexprlemdisj  7903  suplocexprlemub  7906  wrdsymb  11094  ennnfonelemdc  12965  ennnfonelemg  12969  ennnfonelemp1  12972  ennnfonelemhdmp1  12975  ennnfonelemkh  12978  ennnfonelemhf1o  12979  ennnfonelemex  12980  ennnfonelemhom  12981  ctinfomlemom  12993  ctinf  12996  ctiunctlemudc  13003  ctiunctlemf  13004  omctfn  13009  imasival  13334  imasbas  13335  imasplusg  13336  imasmulr  13337  imasaddfnlemg  13342  imasaddvallemg  13343  imasaddflemg  13344  imasmnd2  13480  imasgrp2  13642  mhmid  13647  mhmmnd  13648  mhmfmhm  13649  ghmgrp  13650  ghmfghm  13858  imasring  14022  znunit  14617  znrrg  14618  dvrecap  15381  gausslemma2dlem1f1o  15733  subctctexmid  16325  pw1nct  16328