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  7278  ccatrn  11157  swrdrn  11205  pfxrn  11235  4sqlem11  12940  ennnfonelemfun  13004  ennnfonelemf1  13005  mhmima  13540  ghmrn  13810  conjnmz  13832  tgrest  14859  resttopon  14861  rest0  14869  cnrest2r  14927  cnptoprest2  14930  lmss  14936  txbasval  14957  upxp  14962  uptx  14964  hmeores  15005  unirnblps  15112  unirnbl  15113  lgseisenlem4  15768  uhgredgm  15950  upgredgssen  15953  umgredgssen  15954  edgupgren  15955  edgumgren  15956