Theorem frnd 5357

Description: Deduction form of frn 5356. The range of a mapping. (Contributed by Glauco Siliprandi, 26-Jun-2021.)

Hypothesis

Ref	Expression
frnd.1	|- ( ph -> F : A --> B )

Assertion

Ref	Expression
frnd	|- ( ph -> ran F C_ B )

Proof of Theorem frnd

Step	Hyp	Ref	Expression
1		frnd.1	. 2 |- ( ph -> F : A --> B )
2		frn 5356	. 2 |- ( F : A --> B -> ran F C_ B )
3	1, 2	syl 14	1 |- ( ph -> ran F C_ B )

Syntax hints:   -> wi 4   C_ wss 3121   ran crn 4612   -->wf 5194

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 5202

This theorem is referenced by:  difinfsn  7077  ennnfonelemfun  12372  ennnfonelemf1  12373  mhmima  12706  tgrest  12963  resttopon  12965  rest0  12973  cnrest2r  13031  cnptoprest2  13034  lmss  13040  txbasval  13061  upxp  13066  uptx  13068  hmeores  13109  unirnblps  13216  unirnbl  13217