Theorem frn 5540

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 5379	. 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 3220   ran crn 4773   Fn wfn 5370   -->wf 5371

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 5379

This theorem is referenced by:  frnd  5541  fimass  5548  fco2  5552  fssxp  5553  fimacnvdisj  5574  f00  5582  f0rn0  5585  f1rn  5597  f1ff1  5604  fimacnv  5831  ffvelcdm  5835  f1ompt  5853  fnfvrnss  5862  rnmptss  5863  fliftrel  5991  fo1stresm  6388  fo2ndresm  6389  1stcof  6390  2ndcof  6391  fo2ndf  6456  tposf2  6532  iunon  6548  smores2  6558  map0b  6961  mapsnd  6963  mapsn  6965  f1imaen2g  7073  phplem4dom  7156  isinfinf  7194  updjudhcoinlf  7413  updjudhcoinrg  7414  casef  7421  unirnioo  10357  frecuzrdgdomlem  10835  frecuzrdgfunlem  10837  frecuzrdgtclt  10839  ballotfilemsima  13240  ennnfonelemrn  13291  ctinf  13302  txuni2  15283  blin2  15459  tgqioo  15582  reeff1o  15800  usgredgssen  16320