Theorem forn 5442

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

Syntax hints:   → wi 4   = wceq 1353  ran crn 4628   Fn wfn 5212  –onto→wfo 5215

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 5223

This theorem is referenced by:  dffo2  5443  foima  5444  fodmrnu  5447  f1imacnv  5479  foimacnv  5480  foun  5481  resdif  5484  fococnv2  5488  foelcdmi  5569  cbvfo  5786  cbvexfo  5787  isoini  5819  isoselem  5821  canth  5829  f1opw2  6077  focdmex  6116  bren  6747  en1  6799  fopwdom  6836  mapen  6846  ssenen  6851  phplem4  6855  phplem4on  6867  ordiso2  7034  djuunr  7065  hashfacen  10816  ennnfonelemrn  12420  imasival  12727  imasaddfnlemg  12735  xpsfrn  12769  hmeontr  13816