Theorem frnd 5435

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

Syntax hints:   → wi 4   ⊆ wss 3166  ran crn 4676  ⟶wf 5267

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 5275

This theorem is referenced by:  difinfsn  7202  ccatrn  11065  swrdrn  11110  4sqlem11  12724  ennnfonelemfun  12788  ennnfonelemf1  12789  mhmima  13323  ghmrn  13593  conjnmz  13615  tgrest  14641  resttopon  14643  rest0  14651  cnrest2r  14709  cnptoprest2  14712  lmss  14718  txbasval  14739  upxp  14744  uptx  14746  hmeores  14787  unirnblps  14894  unirnbl  14895  lgseisenlem4  15550