Theorem frnd 5483

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

Syntax hints:   → wi 4   ⊆ wss 3197  ran crn 4720  ⟶wf 5314

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 5322

This theorem is referenced by:  difinfsn  7275  ccatrn  11152  swrdrn  11197  pfxrn  11227  4sqlem11  12932  ennnfonelemfun  12996  ennnfonelemf1  12997  mhmima  13532  ghmrn  13802  conjnmz  13824  tgrest  14851  resttopon  14853  rest0  14861  cnrest2r  14919  cnptoprest2  14922  lmss  14928  txbasval  14949  upxp  14954  uptx  14956  hmeores  14997  unirnblps  15104  unirnbl  15105  lgseisenlem4  15760  uhgredgm  15942  upgredgssen  15945  umgredgssen  15946  edgupgren  15947  edgumgren  15948