Theorem fof 5481

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 3238	. . 3 ⊢ (ran 𝐹 = 𝐵 → ran 𝐹 ⊆ 𝐵)
2	1	anim2i 342	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) → (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
3		df-fo 5265	. 2 ⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
4		df-f 5263	. 2 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
5	2, 3, 4	3imtr4i 201	1 ⊢ (𝐹:𝐴–onto→𝐵 → 𝐹:𝐴⟶𝐵)

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1364   ⊆ wss 3157  ran crn 4665   Fn wfn 5254  ⟶wf 5255  –onto→wfo 5257

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-11 1520  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-in 3163  df-ss 3170  df-f 5263  df-fo 5265

This theorem is referenced by:  fofun  5482  fofn  5483  dffo2  5485  foima  5486  resdif  5527  ffoss  5537  fconstfvm  5781  cocan2  5836  foeqcnvco  5838  focdmex  6174  algrflem  6289  algrflemg  6290  tposf2  6328  mapsn  6751  ssdomg  6839  fopwdom  6899  fidcenumlemrks  7021  fidcenumlemr  7023  ctmlemr  7176  ctm  7177  ctssdclemn0  7178  ctssdccl  7179  ctssdc  7181  enumctlemm  7182  enumct  7183  fodjuomnilemdc  7212  exmidfodomrlemr  7272  exmidfodomrlemrALT  7273  suplocexprlemdisj  7790  suplocexprlemub  7793  wrdsymb  10965  ennnfonelemdc  12627  ennnfonelemg  12631  ennnfonelemp1  12634  ennnfonelemhdmp1  12637  ennnfonelemkh  12640  ennnfonelemhf1o  12641  ennnfonelemex  12642  ennnfonelemhom  12643  ctinfomlemom  12655  ctinf  12658  ctiunctlemudc  12665  ctiunctlemf  12666  omctfn  12671  imasival  12975  imasbas  12976  imasplusg  12977  imasmulr  12978  imasaddfnlemg  12983  imasaddvallemg  12984  imasaddflemg  12985  imasgrp2  13266  mhmid  13271  mhmmnd  13272  mhmfmhm  13273  ghmgrp  13274  ghmfghm  13482  imasring  13646  znunit  14241  znrrg  14242  dvrecap  14975  gausslemma2dlem1f1o  15327  subctctexmid  15671  pw1nct  15674