Theorem forn 5559

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

Syntax hints:   → wi 4   = wceq 1395  ran crn 4724   Fn wfn 5319  –onto→wfo 5322

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 5330

This theorem is referenced by:  dffo2  5560  foima  5561  fodmrnu  5564  f1imacnv  5597  foimacnv  5598  foun  5599  resdif  5602  fococnv2  5606  foelcdmi  5694  cbvfo  5921  cbvexfo  5922  isoini  5954  isoselem  5956  canth  5964  f1opw2  6224  focdmex  6272  bren  6912  en1  6968  fopwdom  7017  mapen  7027  ssenen  7032  phplem4  7036  phplem4on  7049  ordiso2  7225  djuunr  7256  hashfacen  11090  ennnfonelemrn  13030  imasival  13379  imasaddfnlemg  13387  xpsfrn  13423  imasmnd2  13525  imasgrp2  13687  imasrng  13959  imasring  14067  znf1o  14655  znleval  14657  znunit  14663  hmeontr  15027  fsumdvdsmul  15705