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  5926  cbvexfo  5927  isoini  5959  isoselem  5961  canth  5969  f1opw2  6229  focdmex  6277  bren  6917  en1  6973  fopwdom  7022  mapen  7032  ssenen  7037  phplem4  7041  phplem4on  7054  ordiso2  7234  djuunr  7265  hashfacen  11101  ennnfonelemrn  13045  imasival  13394  imasaddfnlemg  13402  xpsfrn  13438  imasmnd2  13540  imasgrp2  13702  imasrng  13975  imasring  14083  znf1o  14671  znleval  14673  znunit  14679  hmeontr  15043  fsumdvdsmul  15721