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

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

Proof of Theorem frn
StepHypRef Expression
1 df-f 5053 . 2 (𝐹:𝐴𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹𝐵))
21simprbi 270 1 (𝐹:𝐴𝐵 → ran 𝐹𝐵)
Colors of variables: wff set class
Syntax hints:  wi 4  wss 3013  ran crn 4468   Fn wfn 5044  wf 5045
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106
This theorem depends on definitions:  df-bi 116  df-f 5053
This theorem is referenced by:  frnd  5205  fco2  5212  fssxp  5213  fimacnvdisj  5230  f00  5237  f0rn0  5240  f1rn  5252  f1ff1  5259  fimacnv  5467  ffvelrn  5471  f1ompt  5489  fnfvrnss  5497  rnmptss  5498  fliftrel  5609  fo1stresm  5970  fo2ndresm  5971  1stcof  5972  2ndcof  5973  fo2ndf  6030  tposf2  6071  iunon  6087  smores2  6097  map0b  6484  mapsn  6487  f1imaen2g  6590  phplem4dom  6658  isinfinf  6693  djuin  6836  updjudhcoinlf  6851  updjudhcoinrg  6852  casef  6859  unirnioo  9539  frecuzrdgdomlem  9973  frecuzrdgfunlem  9975  frecuzrdgtclt  9977  blin2  12218  tgqioo  12321
  Copyright terms: Public domain W3C validator