ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  forn GIF version

Theorem forn 5137
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
StepHypRef Expression
1 df-fo 4936 . 2 (𝐹:𝐴onto𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
21simprbi 264 1 (𝐹:𝐴onto𝐵 → ran 𝐹 = 𝐵)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1259  ran crn 4374   Fn wfn 4925  ontowfo 4928
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104
This theorem depends on definitions:  df-bi 114  df-fo 4936
This theorem is referenced by:  dffo2  5138  foima  5139  fodmrnu  5142  f1imacnv  5171  foimacnv  5172  foun  5173  resdif  5176  fococnv2  5180  cbvfo  5453  cbvexfo  5454  isoini  5485  isoselem  5487  f1opw2  5734  fornex  5770  bren  6259  en1  6310  fopwdom  6341  phplem4  6349  phplem4on  6360  ordiso2  6415
  Copyright terms: Public domain W3C validator