Theorem forn 5550

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

Syntax hints:   → wi 4   = wceq 1395  ran crn 4719   Fn wfn 5312  –onto→wfo 5315

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 5323

This theorem is referenced by:  dffo2  5551  foima  5552  fodmrnu  5555  f1imacnv  5588  foimacnv  5589  foun  5590  resdif  5593  fococnv2  5597  foelcdmi  5685  cbvfo  5908  cbvexfo  5909  isoini  5941  isoselem  5943  canth  5951  f1opw2  6210  focdmex  6258  bren  6893  en1  6949  fopwdom  6993  mapen  7003  ssenen  7008  phplem4  7012  phplem4on  7025  ordiso2  7198  djuunr  7229  hashfacen  11053  ennnfonelemrn  12985  imasival  13334  imasaddfnlemg  13342  xpsfrn  13378  imasmnd2  13480  imasgrp2  13642  imasrng  13914  imasring  14022  znf1o  14609  znleval  14611  znunit  14617  hmeontr  14981  fsumdvdsmul  15659