Theorem frnd 5482

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

Syntax hints:   → wi 4   ⊆ wss 3197  ran crn 4719  ⟶wf 5313

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 5321

This theorem is referenced by:  difinfsn  7263  ccatrn  11139  swrdrn  11184  pfxrn  11214  4sqlem11  12919  ennnfonelemfun  12983  ennnfonelemf1  12984  mhmima  13519  ghmrn  13789  conjnmz  13811  tgrest  14837  resttopon  14839  rest0  14847  cnrest2r  14905  cnptoprest2  14908  lmss  14914  txbasval  14935  upxp  14940  uptx  14942  hmeores  14983  unirnblps  15090  unirnbl  15091  lgseisenlem4  15746  uhgredgm  15928  upgredgssen  15931  umgredgssen  15932  edgupgren  15933  edgumgren  15934