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

Theorem forn 5109
 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 4908 . 2 (𝐹:𝐴onto𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
21simprbi 260 1 (𝐹:𝐴onto𝐵 → ran 𝐹 = 𝐵)
 Colors of variables: wff set class Syntax hints:   → wi 4   = wceq 1243  ran crn 4346   Fn wfn 4897  –onto→wfo 4900 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100 This theorem depends on definitions:  df-bi 110  df-fo 4908 This theorem is referenced by:  dffo2  5110  foima  5111  fodmrnu  5114  f1imacnv  5143  foimacnv  5144  foun  5145  resdif  5148  fococnv2  5152  cbvfo  5425  cbvexfo  5426  isoini  5457  isoselem  5459  f1opw2  5706  fornex  5742  bren  6228  en1  6279  fopwdom  6310  phplem4  6318  phplem4on  6329  ordiso2  6357
 Copyright terms: Public domain W3C validator