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  11299  ccatrn  11391  swrdrn  11443  pfxrn  11473  4sqlem11  13200  ennnfonelemfun  13357  ennnfonelemf1  13358  mhmima  13847  ghmrn  14109  conjnmz  14131  gsump1  14206  tgrest  15319  resttopon  15321  rest0  15329  cnrest2r  15387  cnptoprest2  15390  lmss  15396  txbasval  15417  upxp  15422  uptx  15424  hmeores  15465  unirnblps  15572  unirnbl  15573  lgseisenlem4  16290  uhgredgm  16475  upgredgssen  16478  umgredgssen  16479  edgupgren  16480  edgumgren  16481