Theorem fof 6794

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 3996	. . 3 ⊢ (ran 𝐹 = 𝐵 → ran 𝐹 ⊆ 𝐵)
2	1	anim2i 628	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) → (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
3		df-fo 6544	. 2 ⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
4		df-f 6542	. 2 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
5	2, 3, 4	3imtr4i 295	1 ⊢ (𝐹:𝐴–onto→𝐵 → 𝐹:𝐴⟶𝐵)

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1570   ⊆ wss 3906  ran crn 5664   Fn wfn 6533  ⟶wf 6534  –onto→wfo 6536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-ss 3923  df-f 6542  df-fo 6544

This theorem is referenced by:  fofun  6795  fofn  6796  dffo2  6798  foima  6799  focnvimacdmdm  6806  focofo  6807  resdif  6844  fimacnvinrn  7068  fompt  7115  fconst5  7206  cocan2  7292  foeqcnvco  7300  soisoi  7328  ffoss  7944  focdmex  7954  opco1  8119  opco2  8120  tposf2  8247  smoiso2  8357  mapfoss  8850  ssdomg  8998  fopwdom  9074  unfilem2  9267  fodomfib  9289  fofinf1o  9290  brwdomn0  9532  fowdom  9534  wdomtr  9538  wdomima2g  9549  fodomfi2  10045  wdomfil  10046  alephiso  10083  iunfictbso  10099  cofsmo  10254  isf32lem10  10347  fin1a2lem7  10391  fodomb  10511  iunfo  10524  tskuni  10769  gruima  10788  gruen  10798  axpre-sup  11155  wrdsymb  14581  supcvg  15912  ruclem13  16299  imasval  17566  imasle  17578  imasaddfnlem  17583  imasaddflem  17585  imasvscafn  17592  imasvscaf  17594  imasless  17595  homadm  18098  homacd  18099  dmaf  18107  cdaf  18108  setcepi  18146  imasmnd2  18833  sursubmefmnd  18956  imasgrp2  19122  mhmid  19130  mhmmnd  19131  mhmfmhm  19132  ghmgrp  19133  efgred2  19824  ghmfghm  19901  ghmcyg  19967  gsumval3  19978  gsumzoppg  20015  gsum2dlem2  20042  imasring  20413  znunit  21694  znrrg  21696  cygznlem2a  21698  cygznlem3  21700  cncmp  23530  cnconn  23560  1stcfb  23583  dfac14  23756  qtopval2  23834  qtopuni  23840  qtopid  23843  qtopcld  23851  qtopcn  23852  qtopeu  23854  qtophmeo  23955  elfm3  24088  ovoliunnul  25647  uniiccdif  25718  dchrzrhcl  27387  lgsdchrval  27496  rpvmasumlem  27629  dchrmusum2  27636  dchrvmasumlem3  27641  dchrisum0ff  27649  dchrisum0flblem1  27650  rpvmasum2  27654  dchrisum0re  27655  dchrisum0lem2a  27659  nodense  27834  bdaydmOLD  27921  bdayon  27923  om2noseqlt  28470  om2noseqlt2  28471  om2noseqf1o  28472  noseqrdgfn  28477  bdayn0sf1o  28541  grpocl  30830  grporndm  30840  vafval  30933  smfval  30935  nvgf  30948  vsfval  30963  hhssabloilem  31591  pjhf  32038  elunop  32202  unopf1o  32246  cnvunop  32248  pjinvari  32521  foresf1o  32828  rabfodom  32829  iunrdx  32886  xppreima  32968  gsumpart  33361  imasmhm  33652  imasghm  33653  imasrhm  33654  qtophaus  34204  sigapildsys  34530  carsgclctunlem3  34688  dfscott3  35490  mtyf  36022  poimirlem26  38275  poimirlem27  38276  volsupnfl  38294  cocanfo  38348  exidreslem  38506  rngosn3  38553  rngodm1dm2  38561  founiiun  45877  founiiun0  45888  issalnnd  47039  sge0fodjrnlem  47110  ismeannd  47161  caragenunicl  47218  fcores  47781  fcoresf1lem  47782  fcoresf1  47783  fcoresfo  47785  3f1oss1  47789  fargshiftfo  48168  uptr2  49976