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  7375  djuunr  7406  hashfacen  11284  ballotfilemro  13266  ennnfonelemrn  13310  imasival  13627  imasaddfnlemg  13635  xpsfrn  13671  imasmnd2  13759  imasgrp2  13913  imasrng  14255  imasring  14369  znf1o  14986  znleval  14988  znunit  14994  hmeontr  15414  fsumdvdsmul  16105