Theorem forn 5562

Description: The codomain of an onto function is its range. (Contributed by NM, 3-Aug-1994.)

Assertion

Ref	Expression
forn	⊢ (𝐹:𝐴–onto→𝐵 → ran 𝐹 = 𝐵)

Proof of Theorem forn

Step	Hyp	Ref	Expression
1		df-fo 5332	. 2 ⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
2	1	simprbi 275	1 ⊢ (𝐹:𝐴–onto→𝐵 → ran 𝐹 = 𝐵)

Syntax hints:   → wi 4   = wceq 1397  ran crn 4726   Fn wfn 5321  –onto→wfo 5324

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107

This theorem depends on definitions:  df-bi 117  df-fo 5332

This theorem is referenced by:  dffo2  5563  foima  5564  fodmrnu  5567  f1imacnv  5600  foimacnv  5601  foun  5602  resdif  5605  fococnv2  5609  foelcdmi  5698  cbvfo  5925  cbvexfo  5926  isoini  5958  isoselem  5960  canth  5968  f1opw2  6228  focdmex  6276  bren  6916  en1  6972  fopwdom  7021  mapen  7031  ssenen  7036  phplem4  7040  phplem4on  7053  ordiso2  7233  djuunr  7264  hashfacen  11099  ennnfonelemrn  13039  imasival  13388  imasaddfnlemg  13396  xpsfrn  13432  imasmnd2  13534  imasgrp2  13696  imasrng  13968  imasring  14076  znf1o  14664  znleval  14666  znunit  14672  hmeontr  15036  fsumdvdsmul  15714