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  7441  hashf1lem1  11301  ccatrn  11393  swrdrn  11445  pfxrn  11475  4sqlem11  13203  ennnfonelemfun  13360  ennnfonelemf1  13361  mhmima  13851  ghmrn  14113  conjnmz  14135  cntzmhm  14167  gsump1  14241  psrbaglefifi  15147  tgrest  15361  resttopon  15363  rest0  15371  cnrest2r  15429  cnptoprest2  15432  lmss  15438  txbasval  15459  upxp  15464  uptx  15466  hmeores  15507  unirnblps  15614  unirnbl  15615  lgseisenlem4  16358  uhgredgm  16543  upgredgssen  16546  umgredgssen  16547  edgupgren  16548  edgumgren  16549