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 3980	. . 3 ⊢ (ran 𝐹 = 𝐵 → ran 𝐹 ⊆ 𝐵)
2	1	anim2i 623	. 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 293	1 ⊢ (𝐹:𝐴–onto→𝐵 → 𝐹:𝐴⟶𝐵)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1547   ⊆ wss 3890  ran crn 5626   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 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2732  df-ss 3907  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  7019  fompt  7066  fconst5  7157  cocan2  7243  foeqcnvco  7251  soisoi  7279  ffoss  7895  focdmex  7905  opco1  8069  opco2  8070  tposf2  8197  smoiso2  8306  mapfoss  8796  ssdomg  8944  fopwdom  9020  unfilem2  9213  fodomfib  9236  fodomfibOLD  9238  fofinf1o  9239  brwdomn0  9481  fowdom  9483  wdomtr  9487  wdomima2g  9498  fodomfi2  9980  wdomfil  9981  alephiso  10018  iunfictbso  10034  cofsmo  10189  isf32lem10  10282  fin1a2lem7  10326  fodomb  10446  iunfo  10459  tskuni  10704  gruima  10723  gruen  10733  axpre-sup  11090  wrdsymb  14502  supcvg  15819  ruclem13  16207  imasval  17473  imasle  17485  imasaddfnlem  17490  imasaddflem  17492  imasvscafn  17499  imasvscaf  17501  imasless  17502  homadm  18005  homacd  18006  dmaf  18014  cdaf  18015  setcepi  18053  imasmnd2  18740  sursubmefmnd  18862  imasgrp2  19029  mhmid  19037  mhmmnd  19038  mhmfmhm  19039  ghmgrp  19040  efgred2  19726  ghmfghm  19803  ghmcyg  19869  gsumval3  19880  gsumzoppg  19917  gsum2dlem2  19944  imasring  20308  znunit  21545  znrrg  21547  cygznlem2a  21549  cygznlem3  21551  cncmp  23382  cnconn  23412  1stcfb  23435  dfac14  23608  qtopval2  23686  qtopuni  23692  qtopid  23695  qtopcld  23703  qtopcn  23704  qtopeu  23706  qtophmeo  23807  elfm3  23940  ovoliunnul  25499  uniiccdif  25570  dchrzrhcl  27233  lgsdchrval  27342  rpvmasumlem  27475  dchrmusum2  27482  dchrvmasumlem3  27487  dchrisum0ff  27495  dchrisum0flblem1  27496  rpvmasum2  27500  dchrisum0re  27501  dchrisum0lem2a  27505  nodense  27681  bdaydm  27767  bdayon  27769  om2noseqlt  28316  om2noseqlt2  28317  om2noseqf1o  28318  noseqrdgfn  28323  bdayn0sf1o  28387  grpocl  30596  grporndm  30606  vafval  30699  smfval  30701  nvgf  30714  vsfval  30729  hhssabloilem  31357  pjhf  31804  elunop  31968  unopf1o  32012  cnvunop  32014  pjinvari  32287  foresf1o  32599  rabfodom  32600  iunrdx  32659  xppreima  32744  gsumpart  33151  imasmhm  33444  imasghm  33445  imasrhm  33446  qtophaus  34027  sigapildsys  34353  carsgclctunlem3  34511  mtyf  35787  poimirlem26  38020  poimirlem27  38021  volsupnfl  38039  cocanfo  38093  exidreslem  38251  rngosn3  38298  rngodm1dm2  38306  founiiun  45633  founiiun0  45644  issalnnd  46795  sge0fodjrnlem  46866  ismeannd  46917  caragenunicl  46974  fcores  47537  fcoresf1lem  47538  fcoresf1  47539  fcoresfo  47541  3f1oss1  47545  fargshiftfo  47924  uptr2  49718