Theorem fof 5498

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 3247	. . 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 5277	. 2 |- ( F : A -onto-> B <-> ( F Fn A /\ ran F = B ) )
4		df-f 5275	. 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 1373   C_ wss 3166   ran crn 4676   Fn wfn 5266   -->wf 5267   -onto->wfo 5269

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 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-11 1529  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-in 3172  df-ss 3179  df-f 5275  df-fo 5277

This theorem is referenced by:  fofun  5499  fofn  5500  dffo2  5502  foima  5503  resdif  5544  ffoss  5554  fconstfvm  5802  cocan2  5857  foeqcnvco  5859  focdmex  6200  algrflem  6315  algrflemg  6316  tposf2  6354  mapsn  6777  ssdomg  6870  fopwdom  6933  fidcenumlemrks  7055  fidcenumlemr  7057  ctmlemr  7210  ctm  7211  ctssdclemn0  7212  ctssdccl  7213  ctssdc  7215  enumctlemm  7216  enumct  7217  fodjuomnilemdc  7246  exmidfodomrlemr  7310  exmidfodomrlemrALT  7311  suplocexprlemdisj  7833  suplocexprlemub  7836  wrdsymb  11021  ennnfonelemdc  12770  ennnfonelemg  12774  ennnfonelemp1  12777  ennnfonelemhdmp1  12780  ennnfonelemkh  12783  ennnfonelemhf1o  12784  ennnfonelemex  12785  ennnfonelemhom  12786  ctinfomlemom  12798  ctinf  12801  ctiunctlemudc  12808  ctiunctlemf  12809  omctfn  12814  imasival  13138  imasbas  13139  imasplusg  13140  imasmulr  13141  imasaddfnlemg  13146  imasaddvallemg  13147  imasaddflemg  13148  imasmnd2  13284  imasgrp2  13446  mhmid  13451  mhmmnd  13452  mhmfmhm  13453  ghmgrp  13454  ghmfghm  13662  imasring  13826  znunit  14421  znrrg  14422  dvrecap  15185  gausslemma2dlem1f1o  15537  subctctexmid  15937  pw1nct  15940