Theorem fof 6834

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1537   ⊆ wss 3976  ran crn 5701   Fn wfn 6568  ⟶wf 6569  –onto→wfo 6571

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-ss 3993  df-f 6577  df-fo 6579

This theorem is referenced by:  fofun  6835  fofn  6836  dffo2  6838  foima  6839  focnvimacdmdm  6846  focofo  6847  resdif  6883  fimacnvinrn  7105  fompt  7152  fconst5  7243  cocan2  7328  foeqcnvco  7336  soisoi  7364  ffoss  7986  focdmex  7996  opco1  8164  opco2  8165  tposf2  8291  smoiso2  8425  mapfoss  8910  ssdomg  9060  fopwdom  9146  unfilem2  9372  fodomfib  9397  fodomfibOLD  9399  fofinf1o  9400  brwdomn0  9638  fowdom  9640  wdomtr  9644  wdomima2g  9655  fodomfi2  10129  wdomfil  10130  alephiso  10167  iunfictbso  10183  cofsmo  10338  isf32lem10  10431  fin1a2lem7  10475  fodomb  10595  iunfo  10608  tskuni  10852  gruima  10871  gruen  10881  axpre-sup  11238  wrdsymb  14590  supcvg  15904  ruclem13  16290  imasval  17571  imasle  17583  imasaddfnlem  17588  imasaddflem  17590  imasvscafn  17597  imasvscaf  17599  imasless  17600  homadm  18107  homacd  18108  dmaf  18116  cdaf  18117  setcepi  18155  imasmnd2  18809  sursubmefmnd  18931  imasgrp2  19095  mhmid  19103  mhmmnd  19104  mhmfmhm  19105  ghmgrp  19106  efgred2  19795  ghmfghm  19872  ghmcyg  19938  gsumval3  19949  gsumzoppg  19986  gsum2dlem2  20013  imasring  20353  znunit  21605  znrrg  21607  cygznlem2a  21609  cygznlem3  21611  cncmp  23421  cnconn  23451  1stcfb  23474  dfac14  23647  qtopval2  23725  qtopuni  23731  qtopid  23734  qtopcld  23742  qtopcn  23743  qtopeu  23745  qtophmeo  23846  elfm3  23979  ovoliunnul  25561  uniiccdif  25632  dchrzrhcl  27307  lgsdchrval  27416  rpvmasumlem  27549  dchrmusum2  27556  dchrvmasumlem3  27561  dchrisum0ff  27569  dchrisum0flblem1  27570  rpvmasum2  27574  dchrisum0re  27575  dchrisum0lem2a  27579  nodense  27755  bdaydm  27837  bdayelon  27839  om2noseqlt  28323  om2noseqlt2  28324  om2noseqf1o  28325  noseqrdgfn  28330  grpocl  30532  grporndm  30542  vafval  30635  smfval  30637  nvgf  30650  vsfval  30665  hhssabloilem  31293  pjhf  31740  elunop  31904  unopf1o  31948  cnvunop  31950  pjinvari  32223  foresf1o  32532  rabfodom  32533  iunrdx  32586  xppreima  32664  gsumpart  33038  imasmhm  33347  imasghm  33348  imasrhm  33349  qtophaus  33782  sigapildsys  34126  carsgclctunlem3  34285  mtyf  35520  poimirlem26  37606  poimirlem27  37607  volsupnfl  37625  cocanfo  37679  exidreslem  37837  rngosn3  37884  rngodm1dm2  37892  founiiun  45086  founiiun0  45097  issalnnd  46266  sge0fodjrnlem  46337  ismeannd  46388  caragenunicl  46445  fcores  46982  fcoresf1lem  46983  fcoresf1  46984  fcoresfo  46986  3f1oss1  46990  fargshiftfo  47316