Theorem fof 5590

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 3292	. . 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 5358	. 2 |- ( F : A -onto-> B <-> ( F Fn A /\ ran F = B ) )
4		df-f 5356	. 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 1398   C_ wss 3211   ran crn 4750   Fn wfn 5347   -->wf 5348   -onto->wfo 5350

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-in 3217  df-ss 3224  df-f 5356  df-fo 5358

This theorem is referenced by:  fofun  5591  fofn  5592  dffo2  5594  foima  5595  resdif  5636  ffoss  5647  fconstfvm  5902  cocan2  5961  foeqcnvco  5963  focdmex  6308  algrflem  6425  algrflemg  6426  tposf2  6499  mapsn  6925  ssdomg  7018  fopwdom  7089  fidcenumlemrks  7223  fidcenumlemr  7225  ctmlemr  7399  ctm  7400  ctssdclemn0  7401  ctssdccl  7402  ctssdc  7404  enumctlemm  7405  enumct  7406  fodjuomnilemdc  7435  exmidfodomrlemr  7505  exmidfodomrlemrALT  7506  suplocexprlemdisj  8035  suplocexprlemub  8038  wrdsymb  11252  ennnfonelemdc  13150  ennnfonelemg  13154  ennnfonelemp1  13157  ennnfonelemhdmp1  13160  ennnfonelemkh  13163  ennnfonelemhf1o  13164  ennnfonelemex  13165  ennnfonelemhom  13166  ctinfomlemom  13178  ctinf  13181  ctiunctlemudc  13188  ctiunctlemf  13189  omctfn  13194  imasival  13519  imasbas  13520  imasplusg  13521  imasmulr  13522  imasaddfnlemg  13527  imasaddvallemg  13528  imasaddflemg  13529  imasmnd2  13665  imasgrp2  13827  mhmid  13832  mhmmnd  13833  mhmfmhm  13834  ghmgrp  13835  ghmfghm  14043  imasring  14208  znunit  14807  znrrg  14808  dvrecap  15578  gausslemma2dlem1f1o  15933  subctctexmid  16774  pw1nct  16777