Theorem frnd 5455

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

Syntax hints:   → wi 4   ⊆ wss 3174  ran crn 4694  ⟶wf 5286

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 5294

This theorem is referenced by:  difinfsn  7228  ccatrn  11103  swrdrn  11148  pfxrn  11178  4sqlem11  12839  ennnfonelemfun  12903  ennnfonelemf1  12904  mhmima  13438  ghmrn  13708  conjnmz  13730  tgrest  14756  resttopon  14758  rest0  14766  cnrest2r  14824  cnptoprest2  14827  lmss  14833  txbasval  14854  upxp  14859  uptx  14861  hmeores  14902  unirnblps  15009  unirnbl  15010  lgseisenlem4  15665  uhgredgm  15842  edgupgren  15845  edgumgren  15846