Theorem fof 5505

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

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1373   ⊆ wss 3167  ran crn 4680   Fn wfn 5271  ⟶wf 5272  –onto→wfo 5274

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-11 1530  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-in 3173  df-ss 3180  df-f 5280  df-fo 5282

This theorem is referenced by:  fofun  5506  fofn  5507  dffo2  5509  foima  5510  resdif  5551  ffoss  5561  fconstfvm  5809  cocan2  5864  foeqcnvco  5866  focdmex  6207  algrflem  6322  algrflemg  6323  tposf2  6361  mapsn  6784  ssdomg  6877  fopwdom  6940  fidcenumlemrks  7062  fidcenumlemr  7064  ctmlemr  7217  ctm  7218  ctssdclemn0  7219  ctssdccl  7220  ctssdc  7222  enumctlemm  7223  enumct  7224  fodjuomnilemdc  7253  exmidfodomrlemr  7317  exmidfodomrlemrALT  7318  suplocexprlemdisj  7840  suplocexprlemub  7843  wrdsymb  11028  ennnfonelemdc  12814  ennnfonelemg  12818  ennnfonelemp1  12821  ennnfonelemhdmp1  12824  ennnfonelemkh  12827  ennnfonelemhf1o  12828  ennnfonelemex  12829  ennnfonelemhom  12830  ctinfomlemom  12842  ctinf  12845  ctiunctlemudc  12852  ctiunctlemf  12853  omctfn  12858  imasival  13182  imasbas  13183  imasplusg  13184  imasmulr  13185  imasaddfnlemg  13190  imasaddvallemg  13191  imasaddflemg  13192  imasmnd2  13328  imasgrp2  13490  mhmid  13495  mhmmnd  13496  mhmfmhm  13497  ghmgrp  13498  ghmfghm  13706  imasring  13870  znunit  14465  znrrg  14466  dvrecap  15229  gausslemma2dlem1f1o  15581  subctctexmid  16011  pw1nct  16014