Theorem fof 6753

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1541   ⊆ wss 3908  ran crn 5632   Fn wfn 6488  ⟶wf 6489  –onto→wfo 6491

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 2707

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-v 3445  df-in 3915  df-ss 3925  df-f 6497  df-fo 6499

This theorem is referenced by:  fofun  6754  fofn  6755  dffo2  6757  foima  6758  focnvimacdmdm  6765  focofo  6766  resdif  6802  fimacnvinrn  7019  fconst5  7151  cocan2  7234  foeqcnvco  7242  soisoi  7269  ffoss  7870  focdmex  7880  opco1  8047  opco2  8048  tposf2  8173  smoiso2  8307  mapfoss  8748  ssdomg  8898  fopwdom  8982  unfilem2  9213  fodomfib  9228  fofinf1o  9229  brwdomn0  9463  fowdom  9465  wdomtr  9469  wdomima2g  9480  fodomfi2  9954  wdomfil  9955  alephiso  9992  iunfictbso  10008  cofsmo  10163  isf32lem10  10256  fin1a2lem7  10300  fodomb  10420  iunfo  10433  tskuni  10677  gruima  10696  gruen  10706  axpre-sup  11063  wrdsymb  14384  supcvg  15695  ruclem13  16078  imasval  17347  imasle  17359  imasaddfnlem  17364  imasaddflem  17366  imasvscafn  17373  imasvscaf  17375  imasless  17376  homadm  17880  homacd  17881  dmaf  17889  cdaf  17890  setcepi  17928  imasmnd2  18547  sursubmefmnd  18660  imasgrp2  18815  mhmid  18821  mhmmnd  18822  mhmfmhm  18823  ghmgrp  18824  efgred2  19488  ghmfghm  19562  ghmcyg  19626  gsumval3  19637  gsumzoppg  19674  gsum2dlem2  19701  imasring  19992  znunit  20917  znrrg  20919  cygznlem2a  20921  cygznlem3  20923  cncmp  22689  cnconn  22719  1stcfb  22742  dfac14  22915  qtopval2  22993  qtopuni  22999  qtopid  23002  qtopcld  23010  qtopcn  23011  qtopeu  23013  qtophmeo  23114  elfm3  23247  ovoliunnul  24817  uniiccdif  24888  dchrzrhcl  26539  lgsdchrval  26648  rpvmasumlem  26781  dchrmusum2  26788  dchrvmasumlem3  26793  dchrisum0ff  26801  dchrisum0flblem1  26802  rpvmasum2  26806  dchrisum0re  26807  dchrisum0lem2a  26811  nodense  26986  bdaydm  27060  bdayelon  27062  grpocl  29287  grporndm  29297  vafval  29390  smfval  29392  nvgf  29405  vsfval  29420  hhssabloilem  30048  pjhf  30495  elunop  30659  unopf1o  30703  cnvunop  30705  pjinvari  30978  foresf1o  31276  rabfodom  31277  iunrdx  31327  xppreima  31407  gsumpart  31739  qtophaus  32245  sigapildsys  32589  carsgclctunlem3  32748  mtyf  33974  poimirlem26  36036  poimirlem27  36037  volsupnfl  36055  cocanfo  36109  exidreslem  36268  rngosn3  36315  rngodm1dm2  36323  founiiun  43295  founiiun0  43308  issalnnd  44481  sge0fodjrnlem  44552  ismeannd  44603  caragenunicl  44660  fcores  45196  fcoresf1lem  45197  fcoresf1  45198  fcoresfo  45200  fargshiftfo  45529