Theorem forn 5483

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

Syntax hints:   → wi 4   = wceq 1364  ran crn 4664   Fn wfn 5253  –onto→wfo 5256

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 5264

This theorem is referenced by:  dffo2  5484  foima  5485  fodmrnu  5488  f1imacnv  5521  foimacnv  5522  foun  5523  resdif  5526  fococnv2  5530  foelcdmi  5613  cbvfo  5832  cbvexfo  5833  isoini  5865  isoselem  5867  canth  5875  f1opw2  6129  focdmex  6172  bren  6806  en1  6858  fopwdom  6897  mapen  6907  ssenen  6912  phplem4  6916  phplem4on  6928  ordiso2  7101  djuunr  7132  hashfacen  10928  ennnfonelemrn  12636  imasival  12949  imasaddfnlemg  12957  xpsfrn  12993  imasgrp2  13240  imasrng  13512  imasring  13620  znf1o  14207  znleval  14209  znunit  14215  hmeontr  14549  fsumdvdsmul  15227