Theorem frnd 5377

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

Syntax hints:   → wi 4   ⊆ wss 3131  ran crn 4629  ⟶wf 5214

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 5222

This theorem is referenced by:  difinfsn  7101  ennnfonelemfun  12420  ennnfonelemf1  12421  mhmima  12880  tgrest  13754  resttopon  13756  rest0  13764  cnrest2r  13822  cnptoprest2  13825  lmss  13831  txbasval  13852  upxp  13857  uptx  13859  hmeores  13900  unirnblps  14007  unirnbl  14008