Theorem fof 6416

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 3906	. . 3 ⊢ (ran 𝐹 = 𝐵 → ran 𝐹 ⊆ 𝐵)
2	1	anim2i 608	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) → (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
3		df-fo 6191	. 2 ⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
4		df-f 6189	. 2 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
5	2, 3, 4	3imtr4i 284	1 ⊢ (𝐹:𝐴–onto→𝐵 → 𝐹:𝐴⟶𝐵)

Syntax hints:   → wi 4   ∧ wa 387   = wceq 1508   ⊆ wss 3822  ran crn 5404   Fn wfn 6180  ⟶wf 6181  –onto→wfo 6183

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-ext 2743

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-clab 2752  df-cleq 2764  df-clel 2839  df-in 3829  df-ss 3836  df-f 6189  df-fo 6191

This theorem is referenced by:  fofun  6417  fofn  6418  dffo2  6420  foima  6421  resdif  6461  fimacnvinrn  6663  fconst5  6793  cocan2  6871  foeqcnvco  6879  soisoi  6902  ffoss  7457  fornex  7467  algrflem  7622  tposf2  7717  smoiso2  7808  ssdomg  8350  fopwdom  8419  unfilem2  8576  fodomfib  8591  fofinf1o  8592  brwdomn0  8826  fowdom  8828  wdomtr  8832  wdomima2g  8843  fodomfi2  9278  wdomfil  9279  alephiso  9316  iunfictbso  9332  cofsmo  9487  isf32lem10  9580  fin1a2lem7  9624  fodomb  9744  iunfo  9757  tskuni  10001  gruima  10020  gruen  10030  axpre-sup  10387  focdmex  13524  wrdsymb  13702  supcvg  15069  ruclem13  15453  imasval  16638  imasle  16650  imasaddfnlem  16655  imasaddflem  16657  imasvscafn  16664  imasvscaf  16666  imasless  16667  homadm  17170  homacd  17171  dmaf  17179  cdaf  17180  setcepi  17218  imasmnd2  17807  imasgrp2  18013  mhmid  18019  mhmmnd  18020  mhmfmhm  18021  ghmgrp  18022  efgred2  18651  ghmfghm  18721  ghmcyg  18782  gsumval3  18793  gsumzoppg  18829  gsum2dlem2  18856  imasring  19104  znunit  20427  znrrg  20429  cygznlem2a  20431  cygznlem3  20433  cncmp  21719  cnconn  21749  1stcfb  21772  dfac14  21945  qtopval2  22023  qtopuni  22029  qtopid  22032  qtopcld  22040  qtopcn  22041  qtopeu  22043  qtophmeo  22144  elfm3  22277  ovoliunnul  23826  uniiccdif  23897  dchrzrhcl  25538  lgsdchrval  25647  rpvmasumlem  25780  dchrmusum2  25787  dchrvmasumlem3  25792  dchrisum0ff  25800  dchrisum0flblem1  25801  rpvmasum2  25805  dchrisum0re  25806  dchrisum0lem2a  25810  grpocl  28069  grporndm  28079  vafval  28172  smfval  28174  nvgf  28187  vsfval  28202  hhssabloilem  28832  pjhf  29281  elunop  29445  unopf1o  29489  cnvunop  29491  pjinvari  29764  foresf1o  30059  rabfodom  30060  iunrdx  30101  xppreima  30173  qtophaus  30776  sigapildsys  31098  carsgclctunlem3  31255  mtyf  32356  nodense  32754  bdaydm  32802  bdayelon  32804  poimirlem26  34396  poimirlem27  34397  volsupnfl  34415  cocanfo  34472  exidreslem  34634  rngosn3  34681  rngodm1dm2  34689  founiiun  40894  founiiun0  40910  issalnnd  42093  sge0fodjrnlem  42163  ismeannd  42214  caragenunicl  42271  fargshiftfo  43008