Theorem frnd 5434

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

Syntax hints:   → wi 4   ⊆ wss 3165  ran crn 4675  ⟶wf 5266

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 5274

This theorem is referenced by:  difinfsn  7201  ccatrn  11063  4sqlem11  12695  ennnfonelemfun  12759  ennnfonelemf1  12760  mhmima  13294  ghmrn  13564  conjnmz  13586  tgrest  14612  resttopon  14614  rest0  14622  cnrest2r  14680  cnptoprest2  14683  lmss  14689  txbasval  14710  upxp  14715  uptx  14717  hmeores  14758  unirnblps  14865  unirnbl  14866  lgseisenlem4  15521