Theorem frnd 5499

Description: Deduction form of frn 5498. 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 5498	. 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 3201   ran crn 4732   -->wf 5329

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 5337

This theorem is referenced by:  difinfsn  7359  ccatrn  11252  swrdrn  11304  pfxrn  11334  4sqlem11  13054  ennnfonelemfun  13118  ennnfonelemf1  13119  mhmima  13654  ghmrn  13924  conjnmz  13946  tgrest  14980  resttopon  14982  rest0  14990  cnrest2r  15048  cnptoprest2  15051  lmss  15057  txbasval  15078  upxp  15083  uptx  15085  hmeores  15126  unirnblps  15233  unirnbl  15234  lgseisenlem4  15892  uhgredgm  16077  upgredgssen  16080  umgredgssen  16081  edgupgren  16082  edgumgren  16083  gfsump1  16815