Theorem fof 5553

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

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1395   ⊆ wss 3197  ran crn 4721   Fn wfn 5316  ⟶wf 5317  –onto→wfo 5319

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-in 3203  df-ss 3210  df-f 5325  df-fo 5327

This theorem is referenced by:  fofun  5554  fofn  5555  dffo2  5557  foima  5558  resdif  5599  ffoss  5609  fconstfvm  5864  cocan2  5921  foeqcnvco  5923  focdmex  6269  algrflem  6386  algrflemg  6387  tposf2  6425  mapsn  6850  ssdomg  6943  fopwdom  7010  fidcenumlemrks  7136  fidcenumlemr  7138  ctmlemr  7291  ctm  7292  ctssdclemn0  7293  ctssdccl  7294  ctssdc  7296  enumctlemm  7297  enumct  7298  fodjuomnilemdc  7327  exmidfodomrlemr  7396  exmidfodomrlemrALT  7397  suplocexprlemdisj  7923  suplocexprlemub  7926  wrdsymb  11117  ennnfonelemdc  12991  ennnfonelemg  12995  ennnfonelemp1  12998  ennnfonelemhdmp1  13001  ennnfonelemkh  13004  ennnfonelemhf1o  13005  ennnfonelemex  13006  ennnfonelemhom  13007  ctinfomlemom  13019  ctinf  13022  ctiunctlemudc  13029  ctiunctlemf  13030  omctfn  13035  imasival  13360  imasbas  13361  imasplusg  13362  imasmulr  13363  imasaddfnlemg  13368  imasaddvallemg  13369  imasaddflemg  13370  imasmnd2  13506  imasgrp2  13668  mhmid  13673  mhmmnd  13674  mhmfmhm  13675  ghmgrp  13676  ghmfghm  13884  imasring  14048  znunit  14644  znrrg  14645  dvrecap  15408  gausslemma2dlem1f1o  15760  subctctexmid  16479  pw1nct  16482