Theorem forn 5621

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

This proof depends on syntax axioms:   → wi 4   = wceq 1402  ran crn 4777   Fn wfn 5375  –onto→wfo 5378

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107

This proof depends on definitions:  df-bi 117  df-fo 5386

This theorem is used by:  dffo2  5622  foima  5623  fodmrnu  5626  f1imacnv  5659  foimacnv  5660  foun  5661  resdif  5664  fococnv2  5668  foelcdmi  5758  cbvfo  5994  cbvexfo  5995  isoini  6027  isoselem  6029  canth  6039  f1opw2  6299  focdmex  6348  mapfoss  6952  bren  7036  en1  7092  fopwdom  7142  mapen  7152  ssenen  7158  phplem4  7162  phplem4on  7175  ordiso2  7381  djuunr  7412  hashfacen  11305  ballotfilemro  13323  ennnfonelemrn  13367  imasival  13685  imasaddfnlemg  13693  xpsfrn  13729  imasmnd2  13817  imasgrp2  13971  imasrng  14361  imasring  14477  znf1o  15094  znleval  15096  znunit  15102  hmeontr  15556  fsumdvdsmul  16302