Theorem forn 5553

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

Syntax hints:   → wi 4   = wceq 1395  ran crn 4720   Fn wfn 5313  –onto→wfo 5316

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 5324

This theorem is referenced by:  dffo2  5554  foima  5555  fodmrnu  5558  f1imacnv  5591  foimacnv  5592  foun  5593  resdif  5596  fococnv2  5600  foelcdmi  5688  cbvfo  5915  cbvexfo  5916  isoini  5948  isoselem  5950  canth  5958  f1opw2  6218  focdmex  6266  bren  6903  en1  6959  fopwdom  7005  mapen  7015  ssenen  7020  phplem4  7024  phplem4on  7037  ordiso2  7213  djuunr  7244  hashfacen  11071  ennnfonelemrn  13005  imasival  13354  imasaddfnlemg  13362  xpsfrn  13398  imasmnd2  13500  imasgrp2  13662  imasrng  13934  imasring  14042  znf1o  14630  znleval  14632  znunit  14638  hmeontr  15002  fsumdvdsmul  15680