Theorem fof 5559

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 3281	. . 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 5332	. 2 |- ( F : A -onto-> B <-> ( F Fn A /\ ran F = B ) )
4		df-f 5330	. 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 1397   C_ wss 3200   ran crn 4726   Fn wfn 5321   -->wf 5322   -onto->wfo 5324

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 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-11 1554  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3206  df-ss 3213  df-f 5330  df-fo 5332

This theorem is referenced by:  fofun  5560  fofn  5561  dffo2  5563  foima  5564  resdif  5605  ffoss  5616  fconstfvm  5872  cocan2  5929  foeqcnvco  5931  focdmex  6277  algrflem  6394  algrflemg  6395  tposf2  6434  mapsn  6859  ssdomg  6952  fopwdom  7022  fidcenumlemrks  7152  fidcenumlemr  7154  ctmlemr  7307  ctm  7308  ctssdclemn0  7309  ctssdccl  7310  ctssdc  7312  enumctlemm  7313  enumct  7314  fodjuomnilemdc  7343  exmidfodomrlemr  7413  exmidfodomrlemrALT  7414  suplocexprlemdisj  7940  suplocexprlemub  7943  wrdsymb  11145  ennnfonelemdc  13038  ennnfonelemg  13042  ennnfonelemp1  13045  ennnfonelemhdmp1  13048  ennnfonelemkh  13051  ennnfonelemhf1o  13052  ennnfonelemex  13053  ennnfonelemhom  13054  ctinfomlemom  13066  ctinf  13069  ctiunctlemudc  13076  ctiunctlemf  13077  omctfn  13082  imasival  13407  imasbas  13408  imasplusg  13409  imasmulr  13410  imasaddfnlemg  13415  imasaddvallemg  13416  imasaddflemg  13417  imasmnd2  13553  imasgrp2  13715  mhmid  13720  mhmmnd  13721  mhmfmhm  13722  ghmgrp  13723  ghmfghm  13931  imasring  14096  znunit  14692  znrrg  14693  dvrecap  15456  gausslemma2dlem1f1o  15808  subctctexmid  16652  pw1nct  16655