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

Theorem frnd 5252
Description: Deduction form of frn 5251. The range of a mapping. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
Hypothesis
Ref Expression
frnd.1 (𝜑𝐹:𝐴𝐵)
Assertion
Ref Expression
frnd (𝜑 → ran 𝐹𝐵)

Proof of Theorem frnd
StepHypRef Expression
1 frnd.1 . 2 (𝜑𝐹:𝐴𝐵)
2 frn 5251 . 2 (𝐹:𝐴𝐵 → ran 𝐹𝐵)
31, 2syl 14 1 (𝜑 → ran 𝐹𝐵)
Colors of variables: wff set class
Syntax hints:  wi 4  wss 3041  ran crn 4510  wf 5089
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-f 5097
This theorem is referenced by:  difinfsn  6953  ennnfonelemfun  11857  ennnfonelemf1  11858  tgrest  12265  resttopon  12267  rest0  12275  cnrest2r  12333  cnptoprest2  12336  lmss  12342  txbasval  12363  upxp  12368  uptx  12370  hmeores  12411  unirnblps  12518  unirnbl  12519
  Copyright terms: Public domain W3C validator