Theorem fof 5464

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 3228	. . 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 5248	. 2 |- ( F : A -onto-> B <-> ( F Fn A /\ ran F = B ) )
4		df-f 5246	. 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 3148   ran crn 4652   Fn wfn 5237   -->wf 5238   -onto->wfo 5240

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-11 1517  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2171

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-in 3154  df-ss 3161  df-f 5246  df-fo 5248

This theorem is referenced by:  fofun  5465  fofn  5466  dffo2  5468  foima  5469  resdif  5509  ffoss  5519  fconstfvm  5762  cocan2  5817  foeqcnvco  5819  focdmex  6148  algrflem  6262  algrflemg  6263  tposf2  6301  mapsn  6724  ssdomg  6812  fopwdom  6872  fidcenumlemrks  6991  fidcenumlemr  6993  ctmlemr  7146  ctm  7147  ctssdclemn0  7148  ctssdccl  7149  ctssdc  7151  enumctlemm  7152  enumct  7153  fodjuomnilemdc  7182  exmidfodomrlemr  7241  exmidfodomrlemrALT  7242  suplocexprlemdisj  7759  suplocexprlemub  7762  ennnfonelemdc  12467  ennnfonelemg  12471  ennnfonelemp1  12474  ennnfonelemhdmp1  12477  ennnfonelemkh  12480  ennnfonelemhf1o  12481  ennnfonelemex  12482  ennnfonelemhom  12483  ctinfomlemom  12495  ctinf  12498  ctiunctlemudc  12505  ctiunctlemf  12506  omctfn  12511  imasival  12800  imasbas  12801  imasplusg  12802  imasmulr  12803  imasaddfnlemg  12808  imasaddvallemg  12809  imasaddflemg  12810  imasgrp2  13083  mhmid  13088  mhmmnd  13089  mhmfmhm  13090  ghmgrp  13091  ghmfghm  13298  imasring  13451  dvrecap  14713  subctctexmid  15288  pw1nct  15290