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  11298  ballotfilemro  13315  ennnfonelemrn  13359  imasival  13676  imasaddfnlemg  13684  xpsfrn  13720  imasmnd2  13808  imasgrp2  13962  imasrng  14304  imasring  14418  znf1o  15035  znleval  15037  znunit  15043  hmeontr  15463  fsumdvdsmul  16186