Theorem frn 5419

Description: The range of a mapping. (Contributed by NM, 3-Aug-1994.)

Assertion

Ref	Expression
frn	⊢ (𝐹:𝐴⟶𝐵 → ran 𝐹 ⊆ 𝐵)

Proof of Theorem frn

Step	Hyp	Ref	Expression
1		df-f 5263	. 2 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
2	1	simprbi 275	1 ⊢ (𝐹:𝐴⟶𝐵 → ran 𝐹 ⊆ 𝐵)

Syntax hints:   → wi 4   ⊆ wss 3157  ran crn 4665   Fn wfn 5254  ⟶wf 5255

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 5263

This theorem is referenced by:  frnd  5420  fco2  5427  fssxp  5428  fimacnvdisj  5445  f00  5452  f0rn0  5455  f1rn  5467  f1ff1  5474  fimacnv  5694  ffvelcdm  5698  f1ompt  5716  fnfvrnss  5725  rnmptss  5726  fliftrel  5842  fo1stresm  6228  fo2ndresm  6229  1stcof  6230  2ndcof  6231  fo2ndf  6294  tposf2  6335  iunon  6351  smores2  6361  map0b  6755  mapsn  6758  f1imaen2g  6861  phplem4dom  6932  isinfinf  6967  updjudhcoinlf  7155  updjudhcoinrg  7156  casef  7163  unirnioo  10065  frecuzrdgdomlem  10526  frecuzrdgfunlem  10528  frecuzrdgtclt  10530  ennnfonelemrn  12661  ctinf  12672  txuni2  14576  blin2  14752  tgqioo  14875  reeff1o  15093