Theorem frn 5482

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 5322	. 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 3197   ran crn 4720   Fn wfn 5313   -->wf 5314

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 5322

This theorem is referenced by:  frnd  5483  fimass  5489  fco2  5492  fssxp  5493  fimacnvdisj  5512  f00  5519  f0rn0  5522  f1rn  5534  f1ff1  5541  fimacnv  5766  ffvelcdm  5770  f1ompt  5788  fnfvrnss  5797  rnmptss  5798  fliftrel  5922  fo1stresm  6313  fo2ndresm  6314  1stcof  6315  2ndcof  6316  fo2ndf  6379  tposf2  6420  iunon  6436  smores2  6446  map0b  6842  mapsn  6845  f1imaen2g  6953  phplem4dom  7031  isinfinf  7067  updjudhcoinlf  7258  updjudhcoinrg  7259  casef  7266  unirnioo  10181  frecuzrdgdomlem  10651  frecuzrdgfunlem  10653  frecuzrdgtclt  10655  ennnfonelemrn  13006  ctinf  13017  txuni2  14946  blin2  15122  tgqioo  15245  reeff1o  15463  usgredgssen  15976