Theorem frnd 5518

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

Syntax hints:   → wi 4   ⊆ wss 3211  ran crn 4750  ⟶wf 5348

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 5356

This theorem is referenced by:  difinfsn  7391  ccatrn  11297  swrdrn  11349  pfxrn  11379  4sqlem11  13099  ennnfonelemfun  13168  ennnfonelemf1  13169  mhmima  13704  ghmrn  13974  conjnmz  13996  tgrest  15034  resttopon  15036  rest0  15044  cnrest2r  15102  cnptoprest2  15105  lmss  15111  txbasval  15132  upxp  15137  uptx  15139  hmeores  15180  unirnblps  15287  unirnbl  15288  lgseisenlem4  15946  uhgredgm  16131  upgredgssen  16134  umgredgssen  16135  edgupgren  16136  edgumgren  16137  gfsump1  16868