Theorem fof 5483

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  5484  fofn  5485  dffo2  5487  foima  5488  resdif  5529  ffoss  5539  fconstfvm  5783  cocan2  5838  foeqcnvco  5840  focdmex  6181  algrflem  6296  algrflemg  6297  tposf2  6335  mapsn  6758  ssdomg  6846  fopwdom  6906  fidcenumlemrks  7028  fidcenumlemr  7030  ctmlemr  7183  ctm  7184  ctssdclemn0  7185  ctssdccl  7186  ctssdc  7188  enumctlemm  7189  enumct  7190  fodjuomnilemdc  7219  exmidfodomrlemr  7283  exmidfodomrlemrALT  7284  suplocexprlemdisj  7806  suplocexprlemub  7809  wrdsymb  10981  ennnfonelemdc  12643  ennnfonelemg  12647  ennnfonelemp1  12650  ennnfonelemhdmp1  12653  ennnfonelemkh  12656  ennnfonelemhf1o  12657  ennnfonelemex  12658  ennnfonelemhom  12659  ctinfomlemom  12671  ctinf  12674  ctiunctlemudc  12681  ctiunctlemf  12682  omctfn  12687  imasival  13010  imasbas  13011  imasplusg  13012  imasmulr  13013  imasaddfnlemg  13018  imasaddvallemg  13019  imasaddflemg  13020  imasmnd2  13156  imasgrp2  13318  mhmid  13323  mhmmnd  13324  mhmfmhm  13325  ghmgrp  13326  ghmfghm  13534  imasring  13698  znunit  14293  znrrg  14294  dvrecap  15035  gausslemma2dlem1f1o  15387  subctctexmid  15733  pw1nct  15736