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

Theorem frn 5080
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 4934 . 2 (𝐹:𝐴𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹𝐵))
21simprbi 264 1 (𝐹:𝐴𝐵 → ran 𝐹𝐵)
Colors of variables: wff set class
Syntax hints:  wi 4  wss 2945  ran crn 4374   Fn wfn 4925  wf 4926
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104
This theorem depends on definitions:  df-bi 114  df-f 4934
This theorem is referenced by:  fco2  5085  fssxp  5086  fimacnvdisj  5102  f00  5109  fun11iun  5175  fimacnv  5324  ffvelrn  5328  f1ompt  5348  fnfvrnss  5353  rnmptss  5354  fliftrel  5460  f1dmex  5771  fo1stresm  5816  fo2ndresm  5817  1stcof  5818  2ndcof  5819  fo2ndf  5876  tposf2  5914  iunon  5930  smores2  5940  f1imaen2g  6304  phplem4dom  6355  unirnioo  8943
  Copyright terms: Public domain W3C validator