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

Theorem forn 5440
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 5221 . 2 (𝐹:𝐴onto𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
21simprbi 275 1 (𝐹:𝐴onto𝐵 → ran 𝐹 = 𝐵)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1353  ran crn 4626   Fn wfn 5210  ontowfo 5213
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 5221
This theorem is referenced by:  dffo2  5441  foima  5442  fodmrnu  5445  f1imacnv  5477  foimacnv  5478  foun  5479  resdif  5482  fococnv2  5486  foelcdmi  5567  cbvfo  5783  cbvexfo  5784  isoini  5816  isoselem  5818  canth  5826  f1opw2  6074  focdmex  6113  bren  6744  en1  6796  fopwdom  6833  mapen  6843  ssenen  6848  phplem4  6852  phplem4on  6864  ordiso2  7031  djuunr  7062  hashfacen  10809  ennnfonelemrn  12412  hmeontr  13684
  Copyright terms: Public domain W3C validator