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  11306  ccatrn  11398  swrdrn  11450  pfxrn  11480  4sqlem11  13208  ennnfonelemfun  13365  ennnfonelemf1  13366  mhmima  13856  ghmrn  14118  conjnmz  14140  cntzmhm  14172  gsump1  14246  psrbaglefifi  15175  tgrest  15412  resttopon  15414  rest0  15422  cnrest2r  15480  cnptoprest2  15483  lmss  15489  txbasval  15510  upxp  15515  uptx  15517  hmeores  15558  unirnblps  15665  unirnbl  15666  lgseisenlem4  16414  uhgredgm  16599  upgredgssen  16602  umgredgssen  16603  edgupgren  16604  edgumgren  16605