Theorem fof 6746

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 3992	. . 3 ⊢ (ran 𝐹 = 𝐵 → ran 𝐹 ⊆ 𝐵)
2	1	anim2i 617	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) → (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
3		df-fo 6498	. 2 ⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
4		df-f 6496	. 2 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
5	2, 3, 4	3imtr4i 292	1 ⊢ (𝐹:𝐴–onto→𝐵 → 𝐹:𝐴⟶𝐵)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ⊆ wss 3901  ran crn 5625   Fn wfn 6487  ⟶wf 6488  –onto→wfo 6490

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2728  df-ss 3918  df-f 6496  df-fo 6498

This theorem is referenced by:  fofun  6747  fofn  6748  dffo2  6750  foima  6751  focnvimacdmdm  6758  focofo  6759  resdif  6795  fimacnvinrn  7016  fompt  7063  fconst5  7152  cocan2  7238  foeqcnvco  7246  soisoi  7274  ffoss  7890  focdmex  7900  opco1  8065  opco2  8066  tposf2  8192  smoiso2  8301  mapfoss  8789  ssdomg  8937  fopwdom  9013  unfilem2  9206  fodomfib  9229  fodomfibOLD  9231  fofinf1o  9232  brwdomn0  9474  fowdom  9476  wdomtr  9480  wdomima2g  9491  fodomfi2  9970  wdomfil  9971  alephiso  10008  iunfictbso  10024  cofsmo  10179  isf32lem10  10272  fin1a2lem7  10316  fodomb  10436  iunfo  10449  tskuni  10694  gruima  10713  gruen  10723  axpre-sup  11080  wrdsymb  14465  supcvg  15779  ruclem13  16167  imasval  17432  imasle  17444  imasaddfnlem  17449  imasaddflem  17451  imasvscafn  17458  imasvscaf  17460  imasless  17461  homadm  17964  homacd  17965  dmaf  17973  cdaf  17974  setcepi  18012  imasmnd2  18699  sursubmefmnd  18821  imasgrp2  18985  mhmid  18993  mhmmnd  18994  mhmfmhm  18995  ghmgrp  18996  efgred2  19682  ghmfghm  19759  ghmcyg  19825  gsumval3  19836  gsumzoppg  19873  gsum2dlem2  19900  imasring  20266  znunit  21518  znrrg  21520  cygznlem2a  21522  cygznlem3  21524  cncmp  23336  cnconn  23366  1stcfb  23389  dfac14  23562  qtopval2  23640  qtopuni  23646  qtopid  23649  qtopcld  23657  qtopcn  23658  qtopeu  23660  qtophmeo  23761  elfm3  23894  ovoliunnul  25464  uniiccdif  25535  dchrzrhcl  27212  lgsdchrval  27321  rpvmasumlem  27454  dchrmusum2  27461  dchrvmasumlem3  27466  dchrisum0ff  27474  dchrisum0flblem1  27475  rpvmasum2  27479  dchrisum0re  27480  dchrisum0lem2a  27484  nodense  27660  bdaydm  27746  bdayon  27748  om2noseqlt  28295  om2noseqlt2  28296  om2noseqf1o  28297  noseqrdgfn  28302  bdayn0sf1o  28366  grpocl  30575  grporndm  30585  vafval  30678  smfval  30680  nvgf  30693  vsfval  30708  hhssabloilem  31336  pjhf  31783  elunop  31947  unopf1o  31991  cnvunop  31993  pjinvari  32266  foresf1o  32579  rabfodom  32580  iunrdx  32638  xppreima  32723  gsumpart  33146  imasmhm  33435  imasghm  33436  imasrhm  33437  qtophaus  33993  sigapildsys  34319  carsgclctunlem3  34477  mtyf  35746  poimirlem26  37843  poimirlem27  37844  volsupnfl  37862  cocanfo  37916  exidreslem  38074  rngosn3  38121  rngodm1dm2  38129  founiiun  45419  founiiun0  45430  issalnnd  46585  sge0fodjrnlem  46656  ismeannd  46707  caragenunicl  46764  fcores  47309  fcoresf1lem  47310  fcoresf1  47311  fcoresfo  47313  3f1oss1  47317  fargshiftfo  47684  uptr2  49462