Theorem forn 5249

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

Syntax hints:   → wi 4   = wceq 1290  ran crn 4453   Fn wfn 5023  –onto→wfo 5026

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

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

This theorem is referenced by:  dffo2  5250  foima  5251  fodmrnu  5254  f1imacnv  5283  foimacnv  5284  foun  5285  resdif  5288  fococnv2  5292  cbvfo  5578  cbvexfo  5579  isoini  5611  isoselem  5613  f1opw2  5864  fornex  5900  bren  6518  en1  6570  fopwdom  6606  mapen  6616  ssenen  6621  phplem4  6625  phplem4on  6637  ordiso2  6782  djuunr  6812  focdmex  10256  hashfacen  10302