Theorem forn 5613

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

Syntax hints:   → wi 4   = wceq 1402  ran crn 4770   Fn wfn 5367  –onto→wfo 5370

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 5378

This theorem is referenced by:  dffo2  5614  foima  5615  fodmrnu  5618  f1imacnv  5651  foimacnv  5652  foun  5653  resdif  5656  fococnv2  5660  foelcdmi  5749  cbvfo  5981  cbvexfo  5982  isoini  6014  isoselem  6016  canth  6026  f1opw2  6286  focdmex  6334  mapfoss  6937  bren  7020  en1  7076  fopwdom  7126  mapen  7136  ssenen  7142  phplem4  7146  phplem4on  7159  ordiso2  7365  djuunr  7396  hashfacen  11262  ballotfilemro  13244  ennnfonelemrn  13288  imasival  13604  imasaddfnlemg  13612  xpsfrn  13648  imasmnd2  13736  imasgrp2  13890  imasrng  14230  imasring  14342  znf1o  14958  znleval  14960  znunit  14966  hmeontr  15337  fsumdvdsmul  16019