Theorem frn 5376

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 5222	. 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 3131   ran crn 4629   Fn wfn 5213   -->wf 5214

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 5222

This theorem is referenced by:  frnd  5377  fco2  5384  fssxp  5385  fimacnvdisj  5402  f00  5409  f0rn0  5412  f1rn  5424  f1ff1  5431  fimacnv  5647  ffvelcdm  5651  f1ompt  5669  fnfvrnss  5678  rnmptss  5679  fliftrel  5795  fo1stresm  6164  fo2ndresm  6165  1stcof  6166  2ndcof  6167  fo2ndf  6230  tposf2  6271  iunon  6287  smores2  6297  map0b  6689  mapsn  6692  f1imaen2g  6795  phplem4dom  6864  isinfinf  6899  updjudhcoinlf  7081  updjudhcoinrg  7082  casef  7089  unirnioo  9975  frecuzrdgdomlem  10419  frecuzrdgfunlem  10421  frecuzrdgtclt  10423  ennnfonelemrn  12422  ctinf  12433  txuni2  13841  blin2  14017  tgqioo  14132  reeff1o  14279