Theorem frnd 5489

Description: Deduction form of frn 5488. The range of a mapping. (Contributed by Glauco Siliprandi, 26-Jun-2021.)

Hypothesis

Ref	Expression
frnd.1	⊢ (𝜑 → 𝐹:𝐴⟶𝐵)

Assertion

Ref	Expression
frnd	⊢ (𝜑 → ran 𝐹 ⊆ 𝐵)

Proof of Theorem frnd

Step	Hyp	Ref	Expression
1		frnd.1	. 2 ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
2		frn 5488	. 2 ⊢ (𝐹:𝐴⟶𝐵 → ran 𝐹 ⊆ 𝐵)
3	1, 2	syl 14	1 ⊢ (𝜑 → ran 𝐹 ⊆ 𝐵)

Syntax hints:   → wi 4   ⊆ wss 3198  ran crn 4724  ⟶wf 5320

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 5328

This theorem is referenced by:  difinfsn  7290  ccatrn  11176  swrdrn  11228  pfxrn  11258  4sqlem11  12964  ennnfonelemfun  13028  ennnfonelemf1  13029  mhmima  13564  ghmrn  13834  conjnmz  13856  tgrest  14883  resttopon  14885  rest0  14893  cnrest2r  14951  cnptoprest2  14954  lmss  14960  txbasval  14981  upxp  14986  uptx  14988  hmeores  15029  unirnblps  15136  unirnbl  15137  lgseisenlem4  15792  uhgredgm  15975  upgredgssen  15978  umgredgssen  15979  edgupgren  15980  edgumgren  15981