Theorem frnd 5543

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

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3220  ran crn 4775  ⟶wf 5373

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107

This proof depends on definitions:  df-bi 117  df-f 5381

This theorem is used by:  difinfsn  7440  hashf1lem1  11285  ccatrn  11377  swrdrn  11429  pfxrn  11459  4sqlem11  13180  ennnfonelemfun  13308  ennnfonelemf1  13309  mhmima  13798  ghmrn  14060  conjnmz  14082  gsump1  14157  tgrest  15270  resttopon  15272  rest0  15280  cnrest2r  15338  cnptoprest2  15341  lmss  15347  txbasval  15368  upxp  15373  uptx  15375  hmeores  15416  unirnblps  15523  unirnbl  15524  lgseisenlem4  16192  uhgredgm  16377  upgredgssen  16380  umgredgssen  16381  edgupgren  16382  edgumgren  16383