Theorem frnd 5437

Description: Deduction form of frn 5436. 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 5436	. 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 3166   ran crn 4677   -->wf 5268

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 5276

This theorem is referenced by:  difinfsn  7204  ccatrn  11068  swrdrn  11113  pfxrn  11141  4sqlem11  12757  ennnfonelemfun  12821  ennnfonelemf1  12822  mhmima  13356  ghmrn  13626  conjnmz  13648  tgrest  14674  resttopon  14676  rest0  14684  cnrest2r  14742  cnptoprest2  14745  lmss  14751  txbasval  14772  upxp  14777  uptx  14779  hmeores  14820  unirnblps  14927  unirnbl  14928  lgseisenlem4  15583