Theorem forn 5593

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 5358	. 2 ⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
2	1	simprbi 275	1 ⊢ (𝐹:𝐴–onto→𝐵 → ran 𝐹 = 𝐵)

Syntax hints:   → wi 4   = wceq 1398  ran crn 4750   Fn wfn 5347  –onto→wfo 5350

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 5358

This theorem is referenced by:  dffo2  5594  foima  5595  fodmrnu  5598  f1imacnv  5631  foimacnv  5632  foun  5633  resdif  5636  fococnv2  5640  foelcdmi  5729  cbvfo  5958  cbvexfo  5959  isoini  5991  isoselem  5993  canth  6001  f1opw2  6261  focdmex  6308  bren  6983  en1  7039  fopwdom  7089  mapen  7099  ssenen  7105  phplem4  7109  phplem4on  7122  ordiso2  7326  djuunr  7357  hashfacen  11208  ennnfonelemrn  13170  imasival  13519  imasaddfnlemg  13527  xpsfrn  13563  imasmnd2  13665  imasgrp2  13827  imasrng  14100  imasring  14208  znf1o  14799  znleval  14801  znunit  14807  hmeontr  15178  fsumdvdsmul  15859