Theorem frnd 5546

Description: Deduction form of frn 5545. 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 5545	. 2 |- ( F : A --> B -> ran F C_ B )
3	1, 2	syl 14	1 |- ( ph -> ran F C_ B )

This proof depends on syntax axioms:   -> wi 4   C_ wss 3220   ran crn 4777   -->wf 5376

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107

This proof depends on definitions:  df-bi 117  df-f 5384

This theorem is used by:  difinfsn  7446  hashf1lem1  11307  ccatrn  11399  swrdrn  11451  pfxrn  11481  4sqlem11  13209  ennnfonelemfun  13366  ennnfonelemf1  13367  mhmima  13857  ghmrn  14119  conjnmz  14141  cntzmhm  14173  gsump1  14247  psrbaglefifi  15172  tgrest  15395  resttopon  15397  rest0  15405  cnrest2r  15463  cnptoprest2  15466  lmss  15472  txbasval  15493  upxp  15498  uptx  15500  hmeores  15541  unirnblps  15648  unirnbl  15649  lgseisenlem4  16397  uhgredgm  16582  upgredgssen  16585  umgredgssen  16586  edgupgren  16587  edgumgren  16588