Theorem frn 5052

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 4906	. 2 |- ( F : A --> B <-> ( F Fn A /\ ran F C_ B ) )
2	1	simprbi 260	1 |- ( F : A --> B -> ran F C_ B )

Syntax hints:   -> wi 4   C_ wss 2917   ran crn 4346   Fn wfn 4897   -->wf 4898

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100

This theorem depends on definitions:  df-bi 110  df-f 4906

This theorem is referenced by:  fco2  5057  fssxp  5058  fimacnvdisj  5074  f00  5081  fun11iun  5147  fimacnv  5296  ffvelrn  5300  f1ompt  5320  fnfvrnss  5325  rnmptss  5326  fliftrel  5432  f1dmex  5743  fo1stresm  5788  fo2ndresm  5789  1stcof  5790  2ndcof  5791  fo2ndf  5848  tposf2  5883  iunon  5899  smores2  5909  f1imaen2g  6273  phplem4dom  6324  unirnioo  8842