Theorem frn 5072

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

Syntax hints:   -> wi 4   C_ wss 2973   ran crn 4364   Fn wfn 4917   -->wf 4918

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

This theorem depends on definitions:  df-bi 115  df-f 4926

This theorem is referenced by:  fco2  5077  fssxp  5078  fimacnvdisj  5094  f00  5101  fun11iun  5167  fimacnv  5317  ffvelrn  5321  f1ompt  5341  fnfvrnss  5346  rnmptss  5347  fliftrel  5452  f1dmex  5763  fo1stresm  5808  fo2ndresm  5809  1stcof  5810  2ndcof  5811  fo2ndf  5868  tposf2  5906  iunon  5922  smores2  5932  f1imaen2g  6296  phplem4dom  6348  unirnioo  8996