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  12597  ennnfonelemfun  12661  ennnfonelemf1  12662  mhmima  13195  ghmrn  13465  conjnmz  13487  tgrest  14513  resttopon  14515  rest0  14523  cnrest2r  14581  cnptoprest2  14584  lmss  14590  txbasval  14611  upxp  14616  uptx  14618  hmeores  14659  unirnblps  14766  unirnbl  14767  lgseisenlem4  15422