Theorem fof 6752

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ⊆ wss 3889  ran crn 5632   Fn wfn 6493  ⟶wf 6494  –onto→wfo 6496

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728  df-ss 3906  df-f 6502  df-fo 6504

This theorem is referenced by:  fofun  6753  fofn  6754  dffo2  6756  foima  6757  focnvimacdmdm  6764  focofo  6765  resdif  6801  fimacnvinrn  7023  fompt  7070  fconst5  7161  cocan2  7247  foeqcnvco  7255  soisoi  7283  ffoss  7899  focdmex  7909  opco1  8073  opco2  8074  tposf2  8200  smoiso2  8309  mapfoss  8799  ssdomg  8947  fopwdom  9023  unfilem2  9216  fodomfib  9239  fodomfibOLD  9241  fofinf1o  9242  brwdomn0  9484  fowdom  9486  wdomtr  9490  wdomima2g  9501  fodomfi2  9982  wdomfil  9983  alephiso  10020  iunfictbso  10036  cofsmo  10191  isf32lem10  10284  fin1a2lem7  10328  fodomb  10448  iunfo  10461  tskuni  10706  gruima  10725  gruen  10735  axpre-sup  11092  wrdsymb  14504  supcvg  15821  ruclem13  16209  imasval  17475  imasle  17487  imasaddfnlem  17492  imasaddflem  17494  imasvscafn  17501  imasvscaf  17503  imasless  17504  homadm  18007  homacd  18008  dmaf  18016  cdaf  18017  setcepi  18055  imasmnd2  18742  sursubmefmnd  18864  imasgrp2  19031  mhmid  19039  mhmmnd  19040  mhmfmhm  19041  ghmgrp  19042  efgred2  19728  ghmfghm  19805  ghmcyg  19871  gsumval3  19882  gsumzoppg  19919  gsum2dlem2  19946  imasring  20310  znunit  21543  znrrg  21545  cygznlem2a  21547  cygznlem3  21549  cncmp  23357  cnconn  23387  1stcfb  23410  dfac14  23583  qtopval2  23661  qtopuni  23667  qtopid  23670  qtopcld  23678  qtopcn  23679  qtopeu  23681  qtophmeo  23782  elfm3  23915  ovoliunnul  25474  uniiccdif  25545  dchrzrhcl  27208  lgsdchrval  27317  rpvmasumlem  27450  dchrmusum2  27457  dchrvmasumlem3  27462  dchrisum0ff  27470  dchrisum0flblem1  27471  rpvmasum2  27475  dchrisum0re  27476  dchrisum0lem2a  27480  nodense  27656  bdaydm  27742  bdayon  27744  om2noseqlt  28291  om2noseqlt2  28292  om2noseqf1o  28293  noseqrdgfn  28298  bdayn0sf1o  28362  grpocl  30571  grporndm  30581  vafval  30674  smfval  30676  nvgf  30689  vsfval  30704  hhssabloilem  31332  pjhf  31779  elunop  31943  unopf1o  31987  cnvunop  31989  pjinvari  32262  foresf1o  32574  rabfodom  32575  iunrdx  32633  xppreima  32718  gsumpart  33124  imasmhm  33414  imasghm  33415  imasrhm  33416  qtophaus  33980  sigapildsys  34306  carsgclctunlem3  34464  mtyf  35734  poimirlem26  37967  poimirlem27  37968  volsupnfl  37986  cocanfo  38040  exidreslem  38198  rngosn3  38245  rngodm1dm2  38253  founiiun  45609  founiiun0  45620  issalnnd  46773  sge0fodjrnlem  46844  ismeannd  46895  caragenunicl  46952  fcores  47515  fcoresf1lem  47516  fcoresf1  47517  fcoresfo  47519  3f1oss1  47523  fargshiftfo  47902  uptr2  49696