Theorem fof 5595

Description: An onto mapping is a mapping. (Contributed by NM, 3-Aug-1994.)

Assertion

Ref	Expression
fof	⊢ (𝐹:𝐴–onto→𝐵 → 𝐹:𝐴⟶𝐵)

Proof of Theorem fof

Step	Hyp	Ref	Expression
1		eqimss 3296	. . 3 ⊢ (ran 𝐹 = 𝐵 → ran 𝐹 ⊆ 𝐵)
2	1	anim2i 342	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) → (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
3		df-fo 5363	. 2 ⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
4		df-f 5361	. 2 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
5	2, 3, 4	3imtr4i 201	1 ⊢ (𝐹:𝐴–onto→𝐵 → 𝐹:𝐴⟶𝐵)

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1398   ⊆ wss 3214  ran crn 4755   Fn wfn 5352  ⟶wf 5353  –onto→wfo 5355

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 2216

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-in 3220  df-ss 3227  df-f 5361  df-fo 5363

This theorem is referenced by:  fofun  5596  fofn  5597  dffo2  5599  foima  5600  resdif  5641  ffoss  5652  fconstfvm  5907  cocan2  5967  foeqcnvco  5969  focdmex  6317  algrflem  6438  algrflemg  6439  tposf2  6512  mapsn  6938  ssdomg  7031  fopwdom  7102  fidcenumlemrks  7236  fidcenumlemr  7238  ctmlemr  7412  ctm  7413  ctssdclemn0  7414  ctssdccl  7415  ctssdc  7417  enumctlemm  7418  enumct  7419  fodjuomnilemdc  7448  exmidfodomrlemr  7518  exmidfodomrlemrALT  7519  suplocexprlemdisj  8051  suplocexprlemub  8054  wrdsymb  11280  ennnfonelemdc  13237  ennnfonelemg  13241  ennnfonelemp1  13244  ennnfonelemhdmp1  13247  ennnfonelemkh  13250  ennnfonelemhf1o  13251  ennnfonelemex  13252  ennnfonelemhom  13253  ctinfomlemom  13265  ctinf  13268  ctiunctlemudc  13275  ctiunctlemf  13276  omctfn  13281  imasival  13573  imasbas  13574  imasplusg  13575  imasmulr  13576  imasaddfnlemg  13581  imasaddvallemg  13582  imasaddflemg  13583  imasmnd2  13710  imasgrp2  13866  mhmid  13871  mhmmnd  13872  mhmfmhm  13873  ghmgrp  13874  ghmfghm  14082  imasring  14310  znunit  14936  znrrg  14937  dvrecap  15707  gausslemma2dlem1f1o  16062  subctctexmid  16913  pw1nct  16916