Theorem fof 5497

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 3246	. . 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 5276	. 2 |- ( F : A -onto-> B <-> ( F Fn A /\ ran F = B ) )
4		df-f 5274	. 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 1372   C_ wss 3165   ran crn 4675   Fn wfn 5265   -->wf 5266   -onto->wfo 5268

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 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-11 1528  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-in 3171  df-ss 3178  df-f 5274  df-fo 5276

This theorem is referenced by:  fofun  5498  fofn  5499  dffo2  5501  foima  5502  resdif  5543  ffoss  5553  fconstfvm  5801  cocan2  5856  foeqcnvco  5858  focdmex  6199  algrflem  6314  algrflemg  6315  tposf2  6353  mapsn  6776  ssdomg  6869  fopwdom  6932  fidcenumlemrks  7054  fidcenumlemr  7056  ctmlemr  7209  ctm  7210  ctssdclemn0  7211  ctssdccl  7212  ctssdc  7214  enumctlemm  7215  enumct  7216  fodjuomnilemdc  7245  exmidfodomrlemr  7309  exmidfodomrlemrALT  7310  suplocexprlemdisj  7832  suplocexprlemub  7835  wrdsymb  11019  ennnfonelemdc  12741  ennnfonelemg  12745  ennnfonelemp1  12748  ennnfonelemhdmp1  12751  ennnfonelemkh  12754  ennnfonelemhf1o  12755  ennnfonelemex  12756  ennnfonelemhom  12757  ctinfomlemom  12769  ctinf  12772  ctiunctlemudc  12779  ctiunctlemf  12780  omctfn  12785  imasival  13109  imasbas  13110  imasplusg  13111  imasmulr  13112  imasaddfnlemg  13117  imasaddvallemg  13118  imasaddflemg  13119  imasmnd2  13255  imasgrp2  13417  mhmid  13422  mhmmnd  13423  mhmfmhm  13424  ghmgrp  13425  ghmfghm  13633  imasring  13797  znunit  14392  znrrg  14393  dvrecap  15156  gausslemma2dlem1f1o  15508  subctctexmid  15899  pw1nct  15902