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  10067  frecuzrdgdomlem  10528  frecuzrdgfunlem  10530  frecuzrdgtclt  10532  ennnfonelemrn  12663  ctinf  12674  txuni2  14600  blin2  14776  tgqioo  14899  reeff1o  15117