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

Theorem frnd 5286
Description: Deduction form of frn 5285. 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 5285 . 2 (𝐹:𝐴𝐵 → ran 𝐹𝐵)
31, 2syl 14 1 (𝜑 → ran 𝐹𝐵)
Colors of variables: wff set class
Syntax hints:  wi 4  wss 3072  ran crn 4544  wf 5123
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 5131
This theorem is referenced by:  difinfsn  6989  ennnfonelemfun  11957  ennnfonelemf1  11958  tgrest  12368  resttopon  12370  rest0  12378  cnrest2r  12436  cnptoprest2  12439  lmss  12445  txbasval  12466  upxp  12471  uptx  12473  hmeores  12514  unirnblps  12621  unirnbl  12622
  Copyright terms: Public domain W3C validator