Theorem frnd 5420

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

Syntax hints:   → wi 4   ⊆ wss 3157  ran crn 4665  ⟶wf 5255

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 5263

This theorem is referenced by:  difinfsn  7175  4sqlem11  12595  ennnfonelemfun  12659  ennnfonelemf1  12660  mhmima  13193  ghmrn  13463  conjnmz  13485  tgrest  14489  resttopon  14491  rest0  14499  cnrest2r  14557  cnptoprest2  14560  lmss  14566  txbasval  14587  upxp  14592  uptx  14594  hmeores  14635  unirnblps  14742  unirnbl  14743  lgseisenlem4  15398