Theorem frnd 5483

Description: Deduction form of frn 5482. 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 5482	. 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 3197   ran crn 4720   -->wf 5314

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 5322

This theorem is referenced by:  difinfsn  7267  ccatrn  11144  swrdrn  11189  pfxrn  11219  4sqlem11  12924  ennnfonelemfun  12988  ennnfonelemf1  12989  mhmima  13524  ghmrn  13794  conjnmz  13816  tgrest  14843  resttopon  14845  rest0  14853  cnrest2r  14911  cnptoprest2  14914  lmss  14920  txbasval  14941  upxp  14946  uptx  14948  hmeores  14989  unirnblps  15096  unirnbl  15097  lgseisenlem4  15752  uhgredgm  15934  upgredgssen  15937  umgredgssen  15938  edgupgren  15939  edgumgren  15940