Theorem fof 6742

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 3974	. . 3 ⊢ (ran 𝐹 = 𝐵 → ran 𝐹 ⊆ 𝐵)
2	1	anim2i 624	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) → (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
3		df-fo 6494	. 2 ⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
4		df-f 6492	. 2 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
5	2, 3, 4	3imtr4i 294	1 ⊢ (𝐹:𝐴–onto→𝐵 → 𝐹:𝐴⟶𝐵)

Syntax hints:   → wi 4   ∧ wa 397   = wceq 1548   ⊆ wss 3884  ran crn 5621   Fn wfn 6483  ⟶wf 6484  –onto→wfo 6486

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-ex 1788  df-cleq 2733  df-ss 3901  df-f 6492  df-fo 6494

This theorem is referenced by:  fofun  6743  fofn  6744  dffo2  6746  foima  6747  focnvimacdmdm  6754  focofo  6755  resdif  6791  fimacnvinrn  7015  fompt  7062  fconst5  7153  cocan2  7239  foeqcnvco  7247  soisoi  7275  ffoss  7890  focdmex  7900  opco1  8064  opco2  8065  tposf2  8192  smoiso2  8302  mapfoss  8793  ssdomg  8941  fopwdom  9017  unfilem2  9210  fodomfib  9233  fodomfibOLD  9235  fofinf1o  9236  brwdomn0  9478  fowdom  9480  wdomtr  9484  wdomima2g  9495  fodomfi2  9977  wdomfil  9978  alephiso  10015  iunfictbso  10031  cofsmo  10187  isf32lem10  10280  fin1a2lem7  10324  fodomb  10444  iunfo  10457  tskuni  10702  gruima  10721  gruen  10731  axpre-sup  11088  wrdsymb  14499  supcvg  15816  ruclem13  16204  imasval  17470  imasle  17482  imasaddfnlem  17487  imasaddflem  17489  imasvscafn  17496  imasvscaf  17498  imasless  17499  homadm  18002  homacd  18003  dmaf  18011  cdaf  18012  setcepi  18050  imasmnd2  18737  sursubmefmnd  18859  imasgrp2  19026  mhmid  19034  mhmmnd  19035  mhmfmhm  19036  ghmgrp  19037  efgred2  19722  ghmfghm  19799  ghmcyg  19865  gsumval3  19876  gsumzoppg  19913  gsum2dlem2  19940  imasring  20304  znunit  21541  znrrg  21543  cygznlem2a  21545  cygznlem3  21547  cncmp  23378  cnconn  23408  1stcfb  23431  dfac14  23604  qtopval2  23682  qtopuni  23688  qtopid  23691  qtopcld  23699  qtopcn  23700  qtopeu  23702  qtophmeo  23803  elfm3  23936  ovoliunnul  25495  uniiccdif  25566  dchrzrhcl  27229  lgsdchrval  27338  rpvmasumlem  27471  dchrmusum2  27478  dchrvmasumlem3  27483  dchrisum0ff  27491  dchrisum0flblem1  27492  rpvmasum2  27496  dchrisum0re  27497  dchrisum0lem2a  27501  nodense  27676  bdaydm  27762  bdayon  27764  om2noseqlt  28311  om2noseqlt2  28312  om2noseqf1o  28313  noseqrdgfn  28318  bdayn0sf1o  28382  grpocl  30591  grporndm  30601  vafval  30694  smfval  30696  nvgf  30709  vsfval  30724  hhssabloilem  31352  pjhf  31799  elunop  31963  unopf1o  32007  cnvunop  32009  pjinvari  32282  foresf1o  32594  rabfodom  32595  iunrdx  32654  xppreima  32739  gsumpart  33146  imasmhm  33439  imasghm  33440  imasrhm  33441  qtophaus  34030  sigapildsys  34356  carsgclctunlem3  34514  mtyf  35793  poimirlem26  38026  poimirlem27  38027  volsupnfl  38045  cocanfo  38099  exidreslem  38257  rngosn3  38304  rngodm1dm2  38312  founiiun  45638  founiiun0  45649  issalnnd  46800  sge0fodjrnlem  46871  ismeannd  46922  caragenunicl  46979  fcores  47542  fcoresf1lem  47543  fcoresf1  47544  fcoresfo  47546  3f1oss1  47550  fargshiftfo  47929  uptr2  49723