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

Theorem forn 5220
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 5008 . 2 (𝐹:𝐴onto𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
21simprbi 269 1 (𝐹:𝐴onto𝐵 → ran 𝐹 = 𝐵)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1289  ran crn 4429   Fn wfn 4997  ontowfo 5000
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105
This theorem depends on definitions:  df-bi 115  df-fo 5008
This theorem is referenced by:  dffo2  5221  foima  5222  fodmrnu  5225  f1imacnv  5254  foimacnv  5255  foun  5256  resdif  5259  fococnv2  5263  cbvfo  5546  cbvexfo  5547  isoini  5579  isoselem  5581  f1opw2  5832  fornex  5868  bren  6444  en1  6496  fopwdom  6532  mapen  6542  ssenen  6547  phplem4  6551  phplem4on  6563  ordiso2  6707  djuunr  6737  focdmex  10160  hashfacen  10206
  Copyright terms: Public domain W3C validator