Theorem forn 5486

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

Syntax hints:   → wi 4   = wceq 1364  ran crn 4665   Fn wfn 5254  –onto→wfo 5257

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 5265

This theorem is referenced by:  dffo2  5487  foima  5488  fodmrnu  5491  f1imacnv  5524  foimacnv  5525  foun  5526  resdif  5529  fococnv2  5533  foelcdmi  5616  cbvfo  5835  cbvexfo  5836  isoini  5868  isoselem  5870  canth  5878  f1opw2  6133  focdmex  6181  bren  6815  en1  6867  fopwdom  6906  mapen  6916  ssenen  6921  phplem4  6925  phplem4on  6937  ordiso2  7110  djuunr  7141  hashfacen  10947  ennnfonelemrn  12663  imasival  13010  imasaddfnlemg  13018  xpsfrn  13054  imasmnd2  13156  imasgrp2  13318  imasrng  13590  imasring  13698  znf1o  14285  znleval  14287  znunit  14293  hmeontr  14657  fsumdvdsmul  15335