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  12712  ennnfonelemg  12716  ennnfonelemp1  12719  ennnfonelemhdmp1  12722  ennnfonelemkh  12725  ennnfonelemhf1o  12726  ennnfonelemex  12727  ennnfonelemhom  12728  ctinfomlemom  12740  ctinf  12743  ctiunctlemudc  12750  ctiunctlemf  12751  omctfn  12756  imasival  13080  imasbas  13081  imasplusg  13082  imasmulr  13083  imasaddfnlemg  13088  imasaddvallemg  13089  imasaddflemg  13090  imasmnd2  13226  imasgrp2  13388  mhmid  13393  mhmmnd  13394  mhmfmhm  13395  ghmgrp  13396  ghmfghm  13604  imasring  13768  znunit  14363  znrrg  14364  dvrecap  15127  gausslemma2dlem1f1o  15479  subctctexmid  15870  pw1nct  15873