Theorem fof 6806

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

Syntax hints:   → wi 4   ∧ wa 397   = wceq 1542   ⊆ wss 3949  ran crn 5678   Fn wfn 6539  ⟶wf 6540  –onto→wfo 6542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966  df-f 6548  df-fo 6550

This theorem is referenced by:  fofun  6807  fofn  6808  dffo2  6810  foima  6811  focnvimacdmdm  6818  focofo  6819  resdif  6855  fimacnvinrn  7074  fconst5  7207  cocan2  7290  foeqcnvco  7298  soisoi  7325  ffoss  7932  focdmex  7942  opco1  8109  opco2  8110  tposf2  8235  smoiso2  8369  mapfoss  8846  ssdomg  8996  fopwdom  9080  unfilem2  9311  fodomfib  9326  fofinf1o  9327  brwdomn0  9564  fowdom  9566  wdomtr  9570  wdomima2g  9581  fodomfi2  10055  wdomfil  10056  alephiso  10093  iunfictbso  10109  cofsmo  10264  isf32lem10  10357  fin1a2lem7  10401  fodomb  10521  iunfo  10534  tskuni  10778  gruima  10797  gruen  10807  axpre-sup  11164  wrdsymb  14492  supcvg  15802  ruclem13  16185  imasval  17457  imasle  17469  imasaddfnlem  17474  imasaddflem  17476  imasvscafn  17483  imasvscaf  17485  imasless  17486  homadm  17990  homacd  17991  dmaf  17999  cdaf  18000  setcepi  18038  imasmnd2  18662  sursubmefmnd  18777  imasgrp2  18938  mhmid  18946  mhmmnd  18947  mhmfmhm  18948  ghmgrp  18949  efgred2  19621  ghmfghm  19698  ghmcyg  19764  gsumval3  19775  gsumzoppg  19812  gsum2dlem2  19839  imasring  20143  znunit  21119  znrrg  21121  cygznlem2a  21123  cygznlem3  21125  cncmp  22896  cnconn  22926  1stcfb  22949  dfac14  23122  qtopval2  23200  qtopuni  23206  qtopid  23209  qtopcld  23217  qtopcn  23218  qtopeu  23220  qtophmeo  23321  elfm3  23454  ovoliunnul  25024  uniiccdif  25095  dchrzrhcl  26748  lgsdchrval  26857  rpvmasumlem  26990  dchrmusum2  26997  dchrvmasumlem3  27002  dchrisum0ff  27010  dchrisum0flblem1  27011  rpvmasum2  27015  dchrisum0re  27016  dchrisum0lem2a  27020  nodense  27195  bdaydm  27276  bdayelon  27278  grpocl  29753  grporndm  29763  vafval  29856  smfval  29858  nvgf  29871  vsfval  29886  hhssabloilem  30514  pjhf  30961  elunop  31125  unopf1o  31169  cnvunop  31171  pjinvari  31444  foresf1o  31742  rabfodom  31743  iunrdx  31795  xppreima  31871  gsumpart  32207  qtophaus  32816  sigapildsys  33160  carsgclctunlem3  33319  mtyf  34543  poimirlem26  36514  poimirlem27  36515  volsupnfl  36533  cocanfo  36587  exidreslem  36745  rngosn3  36792  rngodm1dm2  36800  founiiun  43875  founiiun0  43888  issalnnd  45061  sge0fodjrnlem  45132  ismeannd  45183  caragenunicl  45240  fcores  45777  fcoresf1lem  45778  fcoresf1  45779  fcoresfo  45781  fargshiftfo  46110