Theorem forn 5413

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

Syntax hints:   → wi 4   = wceq 1343  ran crn 4605   Fn wfn 5183  –onto→wfo 5186

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

This theorem depends on definitions:  df-bi 116  df-fo 5194

This theorem is referenced by:  dffo2  5414  foima  5415  fodmrnu  5418  f1imacnv  5449  foimacnv  5450  foun  5451  resdif  5454  fococnv2  5458  cbvfo  5753  cbvexfo  5754  isoini  5786  isoselem  5788  canth  5796  f1opw2  6044  fornex  6083  bren  6713  en1  6765  fopwdom  6802  mapen  6812  ssenen  6817  phplem4  6821  phplem4on  6833  ordiso2  7000  djuunr  7031  focdmex  10700  hashfacen  10749  ennnfonelemrn  12352  hmeontr  12953