Theorem forn 5343

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

Syntax hints:   → wi 4   = wceq 1331  ran crn 4535   Fn wfn 5113  –onto→wfo 5116

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 5124

This theorem is referenced by:  dffo2  5344  foima  5345  fodmrnu  5348  f1imacnv  5377  foimacnv  5378  foun  5379  resdif  5382  fococnv2  5386  cbvfo  5679  cbvexfo  5680  isoini  5712  isoselem  5714  f1opw2  5969  fornex  6006  bren  6634  en1  6686  fopwdom  6723  mapen  6733  ssenen  6738  phplem4  6742  phplem4on  6754  ordiso2  6913  djuunr  6944  focdmex  10526  hashfacen  10572  ennnfonelemrn  11921  hmeontr  12471