Theorem frn 5412

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

Assertion

Ref	Expression
frn	|- ( F : A --> B -> ran F C_ B )

Proof of Theorem frn

Step	Hyp	Ref	Expression
1		df-f 5258	. 2 |- ( F : A --> B <-> ( F Fn A /\ ran F C_ B ) )
2	1	simprbi 275	1 |- ( F : A --> B -> ran F C_ B )

Syntax hints:   -> wi 4   C_ wss 3153   ran crn 4660   Fn wfn 5249   -->wf 5250

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 5258

This theorem is referenced by:  frnd  5413  fco2  5420  fssxp  5421  fimacnvdisj  5438  f00  5445  f0rn0  5448  f1rn  5460  f1ff1  5467  fimacnv  5687  ffvelcdm  5691  f1ompt  5709  fnfvrnss  5718  rnmptss  5719  fliftrel  5835  fo1stresm  6214  fo2ndresm  6215  1stcof  6216  2ndcof  6217  fo2ndf  6280  tposf2  6321  iunon  6337  smores2  6347  map0b  6741  mapsn  6744  f1imaen2g  6847  phplem4dom  6918  isinfinf  6953  updjudhcoinlf  7139  updjudhcoinrg  7140  casef  7147  unirnioo  10039  frecuzrdgdomlem  10488  frecuzrdgfunlem  10490  frecuzrdgtclt  10492  ennnfonelemrn  12576  ctinf  12587  txuni2  14424  blin2  14600  tgqioo  14715  reeff1o  14908