Theorem fof 6746

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ⊆ wss 3890  ran crn 5625   Fn wfn 6487  ⟶wf 6488  –onto→wfo 6490

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 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ss 3907  df-f 6496  df-fo 6498

This theorem is referenced by:  fofun  6747  fofn  6748  dffo2  6750  foima  6751  focnvimacdmdm  6758  focofo  6759  resdif  6795  fimacnvinrn  7017  fompt  7064  fconst5  7154  cocan2  7240  foeqcnvco  7248  soisoi  7276  ffoss  7892  focdmex  7902  opco1  8066  opco2  8067  tposf2  8193  smoiso2  8302  mapfoss  8792  ssdomg  8940  fopwdom  9016  unfilem2  9209  fodomfib  9232  fodomfibOLD  9234  fofinf1o  9235  brwdomn0  9477  fowdom  9479  wdomtr  9483  wdomima2g  9494  fodomfi2  9973  wdomfil  9974  alephiso  10011  iunfictbso  10027  cofsmo  10182  isf32lem10  10275  fin1a2lem7  10319  fodomb  10439  iunfo  10452  tskuni  10697  gruima  10716  gruen  10726  axpre-sup  11083  wrdsymb  14495  supcvg  15812  ruclem13  16200  imasval  17466  imasle  17478  imasaddfnlem  17483  imasaddflem  17485  imasvscafn  17492  imasvscaf  17494  imasless  17495  homadm  17998  homacd  17999  dmaf  18007  cdaf  18008  setcepi  18046  imasmnd2  18733  sursubmefmnd  18855  imasgrp2  19022  mhmid  19030  mhmmnd  19031  mhmfmhm  19032  ghmgrp  19033  efgred2  19719  ghmfghm  19796  ghmcyg  19862  gsumval3  19873  gsumzoppg  19910  gsum2dlem2  19937  imasring  20301  znunit  21553  znrrg  21555  cygznlem2a  21557  cygznlem3  21559  cncmp  23367  cnconn  23397  1stcfb  23420  dfac14  23593  qtopval2  23671  qtopuni  23677  qtopid  23680  qtopcld  23688  qtopcn  23689  qtopeu  23691  qtophmeo  23792  elfm3  23925  ovoliunnul  25484  uniiccdif  25555  dchrzrhcl  27222  lgsdchrval  27331  rpvmasumlem  27464  dchrmusum2  27471  dchrvmasumlem3  27476  dchrisum0ff  27484  dchrisum0flblem1  27485  rpvmasum2  27489  dchrisum0re  27490  dchrisum0lem2a  27494  nodense  27670  bdaydm  27756  bdayon  27758  om2noseqlt  28305  om2noseqlt2  28306  om2noseqf1o  28307  noseqrdgfn  28312  bdayn0sf1o  28376  grpocl  30586  grporndm  30596  vafval  30689  smfval  30691  nvgf  30704  vsfval  30719  hhssabloilem  31347  pjhf  31794  elunop  31958  unopf1o  32002  cnvunop  32004  pjinvari  32277  foresf1o  32589  rabfodom  32590  iunrdx  32648  xppreima  32733  gsumpart  33139  imasmhm  33429  imasghm  33430  imasrhm  33431  qtophaus  33996  sigapildsys  34322  carsgclctunlem3  34480  mtyf  35750  poimirlem26  37981  poimirlem27  37982  volsupnfl  38000  cocanfo  38054  exidreslem  38212  rngosn3  38259  rngodm1dm2  38267  founiiun  45627  founiiun0  45638  issalnnd  46791  sge0fodjrnlem  46862  ismeannd  46913  caragenunicl  46970  fcores  47527  fcoresf1lem  47528  fcoresf1  47529  fcoresfo  47531  3f1oss1  47535  fargshiftfo  47914  uptr2  49708