Theorem frnd 5483

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

Syntax hints:   → wi 4   ⊆ wss 3197  ran crn 4720  ⟶wf 5314

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 5322

This theorem is referenced by:  difinfsn  7278  ccatrn  11157  swrdrn  11204  pfxrn  11234  4sqlem11  12939  ennnfonelemfun  13003  ennnfonelemf1  13004  mhmima  13539  ghmrn  13809  conjnmz  13831  tgrest  14858  resttopon  14860  rest0  14868  cnrest2r  14926  cnptoprest2  14929  lmss  14935  txbasval  14956  upxp  14961  uptx  14963  hmeores  15004  unirnblps  15111  unirnbl  15112  lgseisenlem4  15767  uhgredgm  15949  upgredgssen  15952  umgredgssen  15953  edgupgren  15954  edgumgren  15955