Theorem frnd 5417

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

Syntax hints:   → wi 4   ⊆ wss 3157  ran crn 4664  ⟶wf 5254

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 5262

This theorem is referenced by:  difinfsn  7166  4sqlem11  12570  ennnfonelemfun  12634  ennnfonelemf1  12635  mhmima  13123  ghmrn  13387  conjnmz  13409  tgrest  14405  resttopon  14407  rest0  14415  cnrest2r  14473  cnptoprest2  14476  lmss  14482  txbasval  14503  upxp  14508  uptx  14510  hmeores  14551  unirnblps  14658  unirnbl  14659  lgseisenlem4  15314