Theorem frnd 5492

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

Syntax hints:   → wi 4   ⊆ wss 3200  ran crn 4726  ⟶wf 5322

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 5330

This theorem is referenced by:  difinfsn  7299  ccatrn  11190  swrdrn  11242  pfxrn  11272  4sqlem11  12979  ennnfonelemfun  13043  ennnfonelemf1  13044  mhmima  13579  ghmrn  13849  conjnmz  13871  tgrest  14899  resttopon  14901  rest0  14909  cnrest2r  14967  cnptoprest2  14970  lmss  14976  txbasval  14997  upxp  15002  uptx  15004  hmeores  15045  unirnblps  15152  unirnbl  15153  lgseisenlem4  15808  uhgredgm  15993  upgredgssen  15996  umgredgssen  15997  edgupgren  15998  edgumgren  15999  gfsump1  16713