Theorem frnd 5538

Description: Deduction form of frn 5537. 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 5537	. 2 ⊢ (𝐹:𝐴⟶𝐵 → ran 𝐹 ⊆ 𝐵)
3	1, 2	syl 14	1 ⊢ (𝜑 → ran 𝐹 ⊆ 𝐵)

Syntax hints:   → wi 4   ⊆ wss 3220  ran crn 4770  ⟶wf 5368

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 5376

This theorem is referenced by:  difinfsn  7430  hashf1lem1  11263  ccatrn  11355  swrdrn  11407  pfxrn  11437  4sqlem11  13158  ennnfonelemfun  13286  ennnfonelemf1  13287  mhmima  13775  ghmrn  14037  conjnmz  14059  gsump1  14134  tgrest  15193  resttopon  15195  rest0  15203  cnrest2r  15261  cnptoprest2  15264  lmss  15270  txbasval  15291  upxp  15296  uptx  15298  hmeores  15339  unirnblps  15446  unirnbl  15447  lgseisenlem4  16106  uhgredgm  16291  upgredgssen  16294  umgredgssen  16295  edgupgren  16296  edgumgren  16297