Theorem forn 5423

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

Syntax hints:   → wi 4   = wceq 1348  ran crn 4612   Fn wfn 5193  –onto→wfo 5196

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 5204

This theorem is referenced by:  dffo2  5424  foima  5425  fodmrnu  5428  f1imacnv  5459  foimacnv  5460  foun  5461  resdif  5464  fococnv2  5468  cbvfo  5764  cbvexfo  5765  isoini  5797  isoselem  5799  canth  5807  f1opw2  6055  fornex  6094  bren  6725  en1  6777  fopwdom  6814  mapen  6824  ssenen  6829  phplem4  6833  phplem4on  6845  ordiso2  7012  djuunr  7043  focdmex  10721  hashfacen  10771  ennnfonelemrn  12374  hmeontr  13107