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	⊢ (𝜑 → 𝐹:𝐴⟶𝐵)

Assertion

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

Proof of Theorem frnd

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

Syntax hints:   → wi 4   ⊆ 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  7342  ccatrn  11235  swrdrn  11287  pfxrn  11317  4sqlem11  13037  ennnfonelemfun  13101  ennnfonelemf1  13102  mhmima  13637  ghmrn  13907  conjnmz  13929  tgrest  14963  resttopon  14965  rest0  14973  cnrest2r  15031  cnptoprest2  15034  lmss  15040  txbasval  15061  upxp  15066  uptx  15068  hmeores  15109  unirnblps  15216  unirnbl  15217  lgseisenlem4  15875  uhgredgm  16060  upgredgssen  16063  umgredgssen  16064  edgupgren  16065  edgumgren  16066  gfsump1  16798