Theorem frnd 5394

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

Syntax hints:   → wi 4   ⊆ wss 3144  ran crn 4645  ⟶wf 5231

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 5239

This theorem is referenced by:  difinfsn  7130  4sqlem11  12436  ennnfonelemfun  12471  ennnfonelemf1  12472  mhmima  12958  ghmrn  13213  conjnmz  13235  tgrest  14146  resttopon  14148  rest0  14156  cnrest2r  14214  cnptoprest2  14217  lmss  14223  txbasval  14244  upxp  14249  uptx  14251  hmeores  14292  unirnblps  14399  unirnbl  14400