Theorem forn 5618

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

This proof depends on syntax axioms:   → wi 4   = wceq 1402  ran crn 4775   Fn wfn 5372  –onto→wfo 5375

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107

This proof depends on definitions:  df-bi 117  df-fo 5383

This theorem is used by:  dffo2  5619  foima  5620  fodmrnu  5623  f1imacnv  5656  foimacnv  5657  foun  5658  resdif  5661  fococnv2  5665  foelcdmi  5755  cbvfo  5991  cbvexfo  5992  isoini  6024  isoselem  6026  canth  6036  f1opw2  6296  focdmex  6344  mapfoss  6947  bren  7030  en1  7086  fopwdom  7136  mapen  7146  ssenen  7152  phplem4  7156  phplem4on  7169  ordiso2  7376  djuunr  7407  hashfacen  11300  ballotfilemro  13318  ennnfonelemrn  13362  imasival  13680  imasaddfnlemg  13688  xpsfrn  13724  imasmnd2  13812  imasgrp2  13966  imasrng  14339  imasring  14453  znf1o  15070  znleval  15072  znunit  15078  hmeontr  15505  fsumdvdsmul  16246