Theorem frn 5491

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 5330	. 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 3200   ran crn 4726   Fn wfn 5321   -->wf 5322

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 5330

This theorem is referenced by:  frnd  5492  fimass  5498  fco2  5501  fssxp  5502  fimacnvdisj  5521  f00  5529  f0rn0  5532  f1rn  5544  f1ff1  5551  fimacnv  5777  ffvelcdm  5781  f1ompt  5799  fnfvrnss  5808  rnmptss  5809  fliftrel  5936  fo1stresm  6327  fo2ndresm  6328  1stcof  6329  2ndcof  6330  fo2ndf  6395  tposf2  6437  iunon  6453  smores2  6463  map0b  6859  mapsn  6862  f1imaen2g  6970  phplem4dom  7051  isinfinf  7089  updjudhcoinlf  7282  updjudhcoinrg  7283  casef  7290  unirnioo  10211  frecuzrdgdomlem  10683  frecuzrdgfunlem  10685  frecuzrdgtclt  10687  ennnfonelemrn  13061  ctinf  13072  txuni2  15007  blin2  15183  tgqioo  15306  reeff1o  15524  usgredgssen  16040