Theorem forn 5480

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

Syntax hints:   → wi 4   = wceq 1364  ran crn 4661   Fn wfn 5250  –onto→wfo 5253

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 5261

This theorem is referenced by:  dffo2  5481  foima  5482  fodmrnu  5485  f1imacnv  5518  foimacnv  5519  foun  5520  resdif  5523  fococnv2  5527  foelcdmi  5610  cbvfo  5829  cbvexfo  5830  isoini  5862  isoselem  5864  canth  5872  f1opw2  6126  focdmex  6169  bren  6803  en1  6855  fopwdom  6894  mapen  6904  ssenen  6909  phplem4  6913  phplem4on  6925  ordiso2  7096  djuunr  7127  hashfacen  10910  ennnfonelemrn  12579  imasival  12892  imasaddfnlemg  12900  xpsfrn  12936  imasgrp2  13183  imasrng  13455  imasring  13563  znf1o  14150  znleval  14152  znunit  14158  hmeontr  14492