Theorem forn 5571

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

Syntax hints:   → wi 4   = wceq 1398  ran crn 4732   Fn wfn 5328  –onto→wfo 5331

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 5339

This theorem is referenced by:  dffo2  5572  foima  5573  fodmrnu  5576  f1imacnv  5609  foimacnv  5610  foun  5611  resdif  5614  fococnv2  5618  foelcdmi  5707  cbvfo  5936  cbvexfo  5937  isoini  5969  isoselem  5971  canth  5979  f1opw2  6239  focdmex  6286  bren  6960  en1  7016  fopwdom  7065  mapen  7075  ssenen  7080  phplem4  7084  phplem4on  7097  ordiso2  7277  djuunr  7308  hashfacen  11146  ennnfonelemrn  13103  imasival  13452  imasaddfnlemg  13460  xpsfrn  13496  imasmnd2  13598  imasgrp2  13760  imasrng  14033  imasring  14141  znf1o  14730  znleval  14732  znunit  14738  hmeontr  15107  fsumdvdsmul  15788