Theorem fof 5480

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 3237	. . 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 5264	. 2 |- ( F : A -onto-> B <-> ( F Fn A /\ ran F = B ) )
4		df-f 5262	. 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 1364   C_ wss 3157   ran crn 4664   Fn wfn 5253   -->wf 5254   -onto->wfo 5256

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-11 1520  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-in 3163  df-ss 3170  df-f 5262  df-fo 5264

This theorem is referenced by:  fofun  5481  fofn  5482  dffo2  5484  foima  5485  resdif  5526  ffoss  5536  fconstfvm  5780  cocan2  5835  foeqcnvco  5837  focdmex  6172  algrflem  6287  algrflemg  6288  tposf2  6326  mapsn  6749  ssdomg  6837  fopwdom  6897  fidcenumlemrks  7019  fidcenumlemr  7021  ctmlemr  7174  ctm  7175  ctssdclemn0  7176  ctssdccl  7177  ctssdc  7179  enumctlemm  7180  enumct  7181  fodjuomnilemdc  7210  exmidfodomrlemr  7269  exmidfodomrlemrALT  7270  suplocexprlemdisj  7787  suplocexprlemub  7790  wrdsymb  10962  ennnfonelemdc  12616  ennnfonelemg  12620  ennnfonelemp1  12623  ennnfonelemhdmp1  12626  ennnfonelemkh  12629  ennnfonelemhf1o  12630  ennnfonelemex  12631  ennnfonelemhom  12632  ctinfomlemom  12644  ctinf  12647  ctiunctlemudc  12654  ctiunctlemf  12655  omctfn  12660  imasival  12949  imasbas  12950  imasplusg  12951  imasmulr  12952  imasaddfnlemg  12957  imasaddvallemg  12958  imasaddflemg  12959  imasgrp2  13240  mhmid  13245  mhmmnd  13246  mhmfmhm  13247  ghmgrp  13248  ghmfghm  13456  imasring  13620  znunit  14215  znrrg  14216  dvrecap  14949  gausslemma2dlem1f1o  15301  subctctexmid  15645  pw1nct  15647