Theorem frnd 5367

Description: Deduction form of frn 5366. 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 5366	. 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 3127   ran crn 4621   -->wf 5204

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 5212

This theorem is referenced by:  difinfsn  7089  ennnfonelemfun  12385  ennnfonelemf1  12386  mhmima  12737  tgrest  13240  resttopon  13242  rest0  13250  cnrest2r  13308  cnptoprest2  13311  lmss  13317  txbasval  13338  upxp  13343  uptx  13345  hmeores  13386  unirnblps  13493  unirnbl  13494