Theorem forn 5356

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

Syntax hints:   → wi 4   = wceq 1332  ran crn 4548   Fn wfn 5126  –onto→wfo 5129

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 5137

This theorem is referenced by:  dffo2  5357  foima  5358  fodmrnu  5361  f1imacnv  5392  foimacnv  5393  foun  5394  resdif  5397  fococnv2  5401  cbvfo  5694  cbvexfo  5695  isoini  5727  isoselem  5729  f1opw2  5984  fornex  6021  bren  6649  en1  6701  fopwdom  6738  mapen  6748  ssenen  6753  phplem4  6757  phplem4on  6769  ordiso2  6928  djuunr  6959  focdmex  10565  hashfacen  10611  ennnfonelemrn  11968  hmeontr  12521