Theorem fof 5410

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 3196	. . 3 ⊢ (ran 𝐹 = 𝐵 → ran 𝐹 ⊆ 𝐵)
2	1	anim2i 340	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) → (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
3		df-fo 5194	. 2 ⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
4		df-f 5192	. 2 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
5	2, 3, 4	3imtr4i 200	1 ⊢ (𝐹:𝐴–onto→𝐵 → 𝐹:𝐴⟶𝐵)

Syntax hints:   → wi 4   ∧ wa 103   = wceq 1343   ⊆ wss 3116  ran crn 4605   Fn wfn 5183  ⟶wf 5184  –onto→wfo 5186

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-11 1494  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-in 3122  df-ss 3129  df-f 5192  df-fo 5194

This theorem is referenced by:  fofun  5411  fofn  5412  dffo2  5414  foima  5415  resdif  5454  ffoss  5464  fconstfvm  5703  cocan2  5756  foeqcnvco  5758  fornex  6083  algrflem  6197  algrflemg  6198  tposf2  6236  mapsn  6656  ssdomg  6744  fopwdom  6802  fidcenumlemrks  6918  fidcenumlemr  6920  ctmlemr  7073  ctm  7074  ctssdclemn0  7075  ctssdccl  7076  ctssdc  7078  enumctlemm  7079  enumct  7080  fodjuomnilemdc  7108  exmidfodomrlemr  7158  exmidfodomrlemrALT  7159  suplocexprlemdisj  7661  suplocexprlemub  7664  focdmex  10700  ennnfonelemdc  12332  ennnfonelemg  12336  ennnfonelemp1  12339  ennnfonelemhdmp1  12342  ennnfonelemkh  12345  ennnfonelemhf1o  12346  ennnfonelemex  12347  ennnfonelemhom  12348  ctinfomlemom  12360  ctinf  12363  ctiunctlemudc  12370  ctiunctlemf  12371  omctfn  12376  dvrecap  13317  subctctexmid  13881  pw1nct  13883