Theorem frnd 5492

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

Syntax hints:   → wi 4   ⊆ wss 3200  ran crn 4726  ⟶wf 5322

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 5330

This theorem is referenced by:  difinfsn  7298  ccatrn  11185  swrdrn  11237  pfxrn  11267  4sqlem11  12973  ennnfonelemfun  13037  ennnfonelemf1  13038  mhmima  13573  ghmrn  13843  conjnmz  13865  tgrest  14892  resttopon  14894  rest0  14902  cnrest2r  14960  cnptoprest2  14963  lmss  14969  txbasval  14990  upxp  14995  uptx  14997  hmeores  15038  unirnblps  15145  unirnbl  15146  lgseisenlem4  15801  uhgredgm  15986  upgredgssen  15989  umgredgssen  15990  edgupgren  15991  edgumgren  15992