Theorem frnd 5413

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

Syntax hints:   → wi 4   ⊆ wss 3153  ran crn 4660  ⟶wf 5250

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 5258

This theorem is referenced by:  difinfsn  7159  4sqlem11  12539  ennnfonelemfun  12574  ennnfonelemf1  12575  mhmima  13063  ghmrn  13327  conjnmz  13349  tgrest  14337  resttopon  14339  rest0  14347  cnrest2r  14405  cnptoprest2  14408  lmss  14414  txbasval  14435  upxp  14440  uptx  14442  hmeores  14483  unirnblps  14590  unirnbl  14591  lgseisenlem4  15189