Theorem frn 5542

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

This proof depends on syntax axioms:   -> wi 4   C_ wss 3220   ran crn 4775   Fn wfn 5372   -->wf 5373

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107

This proof depends on definitions:  df-bi 117  df-f 5381

This theorem is used by:  frnd  5543  fimass  5550  fco2  5554  fssxp  5555  fimacnvdisj  5576  f00  5584  f0rn0  5587  f1rn  5599  f1ff1  5606  fimacnv  5837  ffvelcdm  5841  f1ompt  5859  fnfvrnss  5868  rnmptss  5869  fliftrel  5998  fo1stresm  6395  fo2ndresm  6396  1stcof  6397  2ndcof  6398  fo2ndf  6463  tposf2  6539  iunon  6555  smores2  6565  map0b  6968  mapsnd  6970  mapsn  6972  f1imaen2g  7080  phplem4dom  7163  isinfinf  7201  updjudhcoinlf  7420  updjudhcoinrg  7421  casef  7428  unirnioo  10385  frecuzrdgdomlem  10867  frecuzrdgfunlem  10869  frecuzrdgtclt  10871  ballotfilemsima  13308  ennnfonelemrn  13359  ctinf  13370  txuni2  15406  blin2  15582  tgqioo  15705  reeff1o  15923  usgredgssen  16501