Theorem frnd 5492

Description: Deduction form of frn 5491. 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 5491	. 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 3200   ran crn 4726   -->wf 5322

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 5330

This theorem is referenced by:  difinfsn  7299  ccatrn  11190  swrdrn  11242  pfxrn  11272  4sqlem11  12992  ennnfonelemfun  13056  ennnfonelemf1  13057  mhmima  13592  ghmrn  13862  conjnmz  13884  tgrest  14912  resttopon  14914  rest0  14922  cnrest2r  14980  cnptoprest2  14983  lmss  14989  txbasval  15010  upxp  15015  uptx  15017  hmeores  15058  unirnblps  15165  unirnbl  15166  lgseisenlem4  15821  uhgredgm  16006  upgredgssen  16009  umgredgssen  16010  edgupgren  16011  edgumgren  16012  gfsump1  16738