Theorem forn 5500

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

Syntax hints:   → wi 4   = wceq 1372  ran crn 4675   Fn wfn 5265  –onto→wfo 5268

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 5276

This theorem is referenced by:  dffo2  5501  foima  5502  fodmrnu  5505  f1imacnv  5538  foimacnv  5539  foun  5540  resdif  5543  fococnv2  5547  foelcdmi  5630  cbvfo  5853  cbvexfo  5854  isoini  5886  isoselem  5888  canth  5896  f1opw2  6151  focdmex  6199  bren  6834  en1  6890  fopwdom  6932  mapen  6942  ssenen  6947  phplem4  6951  phplem4on  6963  ordiso2  7136  djuunr  7167  hashfacen  10979  ennnfonelemrn  12732  imasival  13080  imasaddfnlemg  13088  xpsfrn  13124  imasmnd2  13226  imasgrp2  13388  imasrng  13660  imasring  13768  znf1o  14355  znleval  14357  znunit  14363  hmeontr  14727  fsumdvdsmul  15405