Theorem fof 5439

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 3210	. . 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 5223	. 2 |- ( F : A -onto-> B <-> ( F Fn A /\ ran F = B ) )
4		df-f 5221	. 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 3130   ran crn 4628   Fn wfn 5212   -->wf 5213   -onto->wfo 5215

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 3136  df-ss 3143  df-f 5221  df-fo 5223

This theorem is referenced by:  fofun  5440  fofn  5441  dffo2  5443  foima  5444  resdif  5484  ffoss  5494  fconstfvm  5735  cocan2  5789  foeqcnvco  5791  focdmex  6116  algrflem  6230  algrflemg  6231  tposf2  6269  mapsn  6690  ssdomg  6778  fopwdom  6836  fidcenumlemrks  6952  fidcenumlemr  6954  ctmlemr  7107  ctm  7108  ctssdclemn0  7109  ctssdccl  7110  ctssdc  7112  enumctlemm  7113  enumct  7114  fodjuomnilemdc  7142  exmidfodomrlemr  7201  exmidfodomrlemrALT  7202  suplocexprlemdisj  7719  suplocexprlemub  7722  ennnfonelemdc  12400  ennnfonelemg  12404  ennnfonelemp1  12407  ennnfonelemhdmp1  12410  ennnfonelemkh  12413  ennnfonelemhf1o  12414  ennnfonelemex  12415  ennnfonelemhom  12416  ctinfomlemom  12428  ctinf  12431  ctiunctlemudc  12438  ctiunctlemf  12439  omctfn  12444  imasival  12727  imasbas  12728  imasplusg  12729  imasmulr  12730  imasaddfnlemg  12735  imasaddvallemg  12736  imasaddflemg  12737  mhmid  12979  mhmmnd  12980  mhmfmhm  12981  ghmgrp  12982  dvrecap  14180  subctctexmid  14753  pw1nct  14755