Theorem frnd 5376

Description: Deduction form of frn 5375. 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 5375	. 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 3130   ran crn 4628   -->wf 5213

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107

This theorem depends on definitions:  df-bi 117  df-f 5221

This theorem is referenced by:  difinfsn  7099  ennnfonelemfun  12418  ennnfonelemf1  12419  mhmima  12875  tgrest  13672  resttopon  13674  rest0  13682  cnrest2r  13740  cnptoprest2  13743  lmss  13749  txbasval  13770  upxp  13775  uptx  13777  hmeores  13818  unirnblps  13925  unirnbl  13926