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

Theorem frn 4995
Description: The range of a mapping. (Contributed by NM, 3-Aug-1994.)
Assertion
Ref Expression
frn (𝐹:AB → ran 𝐹B)

Proof of Theorem frn
StepHypRef Expression
1 df-f 4849 . 2 (𝐹:AB ↔ (𝐹 Fn A ran 𝐹B))
21simprbi 260 1 (𝐹:AB → ran 𝐹B)
Colors of variables: wff set class
Syntax hints:  wi 4  wss 2911  ran crn 4289   Fn wfn 4840  wf 4841
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-f 4849
This theorem is referenced by:  fco2  5000  fssxp  5001  fimacnvdisj  5017  f00  5024  fun11iun  5090  fimacnv  5239  ffvelrn  5243  f1ompt  5263  fnfvrnss  5268  rnmptss  5269  fliftrel  5375  f1dmex  5685  fo1stresm  5730  fo2ndresm  5731  1stcof  5732  2ndcof  5733  fo2ndf  5790  tposf2  5824  iunon  5840  smores2  5850  f1imaen2g  6209  unirnioo  8572
  Copyright terms: Public domain W3C validator