Theorem fof 6761

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1541   ⊆ wss 3913  ran crn 5639   Fn wfn 6496  ⟶wf 6497  –onto→wfo 6499

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3448  df-in 3920  df-ss 3930  df-f 6505  df-fo 6507

This theorem is referenced by:  fofun  6762  fofn  6763  dffo2  6765  foima  6766  focnvimacdmdm  6773  focofo  6774  resdif  6810  fimacnvinrn  7027  fconst5  7160  cocan2  7243  foeqcnvco  7251  soisoi  7278  ffoss  7883  focdmex  7893  opco1  8060  opco2  8061  tposf2  8186  smoiso2  8320  mapfoss  8797  ssdomg  8947  fopwdom  9031  unfilem2  9262  fodomfib  9277  fofinf1o  9278  brwdomn0  9514  fowdom  9516  wdomtr  9520  wdomima2g  9531  fodomfi2  10005  wdomfil  10006  alephiso  10043  iunfictbso  10059  cofsmo  10214  isf32lem10  10307  fin1a2lem7  10351  fodomb  10471  iunfo  10484  tskuni  10728  gruima  10747  gruen  10757  axpre-sup  11114  wrdsymb  14442  supcvg  15752  ruclem13  16135  imasval  17407  imasle  17419  imasaddfnlem  17424  imasaddflem  17426  imasvscafn  17433  imasvscaf  17435  imasless  17436  homadm  17940  homacd  17941  dmaf  17949  cdaf  17950  setcepi  17988  imasmnd2  18607  sursubmefmnd  18720  imasgrp2  18876  mhmid  18882  mhmmnd  18883  mhmfmhm  18884  ghmgrp  18885  efgred2  19549  ghmfghm  19623  ghmcyg  19687  gsumval3  19698  gsumzoppg  19735  gsum2dlem2  19762  imasring  20059  znunit  21007  znrrg  21009  cygznlem2a  21011  cygznlem3  21013  cncmp  22780  cnconn  22810  1stcfb  22833  dfac14  23006  qtopval2  23084  qtopuni  23090  qtopid  23093  qtopcld  23101  qtopcn  23102  qtopeu  23104  qtophmeo  23205  elfm3  23338  ovoliunnul  24908  uniiccdif  24979  dchrzrhcl  26630  lgsdchrval  26739  rpvmasumlem  26872  dchrmusum2  26879  dchrvmasumlem3  26884  dchrisum0ff  26892  dchrisum0flblem1  26893  rpvmasum2  26897  dchrisum0re  26898  dchrisum0lem2a  26902  nodense  27077  bdaydm  27157  bdayelon  27159  grpocl  29505  grporndm  29515  vafval  29608  smfval  29610  nvgf  29623  vsfval  29638  hhssabloilem  30266  pjhf  30713  elunop  30877  unopf1o  30921  cnvunop  30923  pjinvari  31196  foresf1o  31495  rabfodom  31496  iunrdx  31549  xppreima  31629  gsumpart  31967  qtophaus  32506  sigapildsys  32850  carsgclctunlem3  33009  mtyf  34233  poimirlem26  36177  poimirlem27  36178  volsupnfl  36196  cocanfo  36250  exidreslem  36409  rngosn3  36456  rngodm1dm2  36464  founiiun  43518  founiiun0  43531  issalnnd  44706  sge0fodjrnlem  44777  ismeannd  44828  caragenunicl  44885  fcores  45421  fcoresf1lem  45422  fcoresf1  45423  fcoresfo  45425  fargshiftfo  45754