Theorem frnd 5523

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

Syntax hints:   → wi 4   ⊆ wss 3214  ran crn 4755  ⟶wf 5353

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 5361

This theorem is referenced by:  difinfsn  7404  ccatrn  11322  swrdrn  11374  pfxrn  11404  4sqlem11  13124  ennnfonelemfun  13252  ennnfonelemf1  13253  mhmima  13746  ghmrn  14010  conjnmz  14032  gfsump1  14108  tgrest  15160  resttopon  15162  rest0  15170  cnrest2r  15228  cnptoprest2  15231  lmss  15237  txbasval  15258  upxp  15263  uptx  15265  hmeores  15306  unirnblps  15413  unirnbl  15414  lgseisenlem4  16072  uhgredgm  16257  upgredgssen  16260  umgredgssen  16261  edgupgren  16262  edgumgren  16263