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

Theorem forn 5348
 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 5129 . 2 (𝐹:𝐴onto𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
21simprbi 273 1 (𝐹:𝐴onto𝐵 → ran 𝐹 = 𝐵)
 Colors of variables: wff set class Syntax hints:   → wi 4   = wceq 1331  ran crn 4540   Fn wfn 5118  –onto→wfo 5121 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106 This theorem depends on definitions:  df-bi 116  df-fo 5129 This theorem is referenced by:  dffo2  5349  foima  5350  fodmrnu  5353  f1imacnv  5384  foimacnv  5385  foun  5386  resdif  5389  fococnv2  5393  cbvfo  5686  cbvexfo  5687  isoini  5719  isoselem  5721  f1opw2  5976  fornex  6013  bren  6641  en1  6693  fopwdom  6730  mapen  6740  ssenen  6745  phplem4  6749  phplem4on  6761  ordiso2  6920  djuunr  6951  focdmex  10533  hashfacen  10579  ennnfonelemrn  11932  hmeontr  12482
 Copyright terms: Public domain W3C validator