Theorem fof 5438

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 3209	. . 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 5222	. 2 |- ( F : A -onto-> B <-> ( F Fn A /\ ran F = B ) )
4		df-f 5220	. 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 1353   C_ wss 3129   ran crn 4627   Fn wfn 5211   -->wf 5212   -onto->wfo 5214

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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-in 3135  df-ss 3142  df-f 5220  df-fo 5222

This theorem is referenced by:  fofun  5439  fofn  5440  dffo2  5442  foima  5443  resdif  5483  ffoss  5493  fconstfvm  5734  cocan2  5788  foeqcnvco  5790  focdmex  6115  algrflem  6229  algrflemg  6230  tposf2  6268  mapsn  6689  ssdomg  6777  fopwdom  6835  fidcenumlemrks  6951  fidcenumlemr  6953  ctmlemr  7106  ctm  7107  ctssdclemn0  7108  ctssdccl  7109  ctssdc  7111  enumctlemm  7112  enumct  7113  fodjuomnilemdc  7141  exmidfodomrlemr  7200  exmidfodomrlemrALT  7201  suplocexprlemdisj  7718  suplocexprlemub  7721  ennnfonelemdc  12399  ennnfonelemg  12403  ennnfonelemp1  12406  ennnfonelemhdmp1  12409  ennnfonelemkh  12412  ennnfonelemhf1o  12413  ennnfonelemex  12414  ennnfonelemhom  12415  ctinfomlemom  12427  ctinf  12430  ctiunctlemudc  12437  ctiunctlemf  12438  omctfn  12443  imasival  12726  imasbas  12727  imasplusg  12728  imasmulr  12729  imasaddfnlemg  12734  imasaddvallemg  12735  imasaddflemg  12736  mhmid  12978  mhmmnd  12979  mhmfmhm  12980  ghmgrp  12981  dvrecap  14147  subctctexmid  14720  pw1nct  14722