Theorem forn 5440

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

Syntax hints:   → wi 4   = wceq 1353  ran crn 4626   Fn wfn 5210  –onto→wfo 5213

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 5221

This theorem is referenced by:  dffo2  5441  foima  5442  fodmrnu  5445  f1imacnv  5477  foimacnv  5478  foun  5479  resdif  5482  fococnv2  5486  foelcdmi  5567  cbvfo  5783  cbvexfo  5784  isoini  5816  isoselem  5818  canth  5826  f1opw2  6074  focdmex  6113  bren  6744  en1  6796  fopwdom  6833  mapen  6843  ssenen  6848  phplem4  6852  phplem4on  6864  ordiso2  7031  djuunr  7062  hashfacen  10809  ennnfonelemrn  12412  hmeontr  13684