Theorem frnd 5414

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

Syntax hints:   → wi 4   ⊆ wss 3154  ran crn 4661  ⟶wf 5251

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 5259

This theorem is referenced by:  difinfsn  7161  4sqlem11  12542  ennnfonelemfun  12577  ennnfonelemf1  12578  mhmima  13066  ghmrn  13330  conjnmz  13352  tgrest  14348  resttopon  14350  rest0  14358  cnrest2r  14416  cnptoprest2  14419  lmss  14425  txbasval  14446  upxp  14451  uptx  14453  hmeores  14494  unirnblps  14601  unirnbl  14602  lgseisenlem4  15230