Theorem forn 5479

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

Syntax hints:   → wi 4   = wceq 1364  ran crn 4660   Fn wfn 5249  –onto→wfo 5252

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 5260

This theorem is referenced by:  dffo2  5480  foima  5481  fodmrnu  5484  f1imacnv  5517  foimacnv  5518  foun  5519  resdif  5522  fococnv2  5526  foelcdmi  5609  cbvfo  5828  cbvexfo  5829  isoini  5861  isoselem  5863  canth  5871  f1opw2  6124  focdmex  6167  bren  6801  en1  6853  fopwdom  6892  mapen  6902  ssenen  6907  phplem4  6911  phplem4on  6923  ordiso2  7094  djuunr  7125  hashfacen  10907  ennnfonelemrn  12576  imasival  12889  imasaddfnlemg  12897  xpsfrn  12933  imasgrp2  13180  imasrng  13452  imasring  13560  znf1o  14139  znleval  14141  znunit  14147  hmeontr  14481