Theorem frn 5519

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 5358	. 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 3213   ran crn 4752   Fn wfn 5349   -->wf 5350

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 5358

This theorem is referenced by:  frnd  5520  fimass  5527  fco2  5531  fssxp  5532  fimacnvdisj  5553  f00  5561  f0rn0  5564  f1rn  5576  f1ff1  5583  fimacnv  5808  ffvelcdm  5812  f1ompt  5830  fnfvrnss  5839  rnmptss  5840  fliftrel  5967  fo1stresm  6357  fo2ndresm  6358  1stcof  6359  2ndcof  6360  fo2ndf  6425  tposf2  6501  iunon  6517  smores2  6527  map0b  6923  mapsnd  6925  mapsn  6927  f1imaen2g  7035  phplem4dom  7118  isinfinf  7156  updjudhcoinlf  7373  updjudhcoinrg  7374  casef  7381  unirnioo  10309  frecuzrdgdomlem  10783  frecuzrdgfunlem  10785  frecuzrdgtclt  10787  ennnfonelemrn  13187  ctinf  13198  txuni2  15138  blin2  15314  tgqioo  15437  reeff1o  15655  usgredgssen  16174