Theorem forn 5513

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

Syntax hints:   → wi 4   = wceq 1373  ran crn 4684   Fn wfn 5275  –onto→wfo 5278

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 5286

This theorem is referenced by:  dffo2  5514  foima  5515  fodmrnu  5518  f1imacnv  5551  foimacnv  5552  foun  5553  resdif  5556  fococnv2  5560  foelcdmi  5644  cbvfo  5867  cbvexfo  5868  isoini  5900  isoselem  5902  canth  5910  f1opw2  6165  focdmex  6213  bren  6848  en1  6904  fopwdom  6948  mapen  6958  ssenen  6963  phplem4  6967  phplem4on  6979  ordiso2  7152  djuunr  7183  hashfacen  11003  ennnfonelemrn  12865  imasival  13213  imasaddfnlemg  13221  xpsfrn  13257  imasmnd2  13359  imasgrp2  13521  imasrng  13793  imasring  13901  znf1o  14488  znleval  14490  znunit  14496  hmeontr  14860  fsumdvdsmul  15538