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  fco2  5490  fssxp  5491  fimacnvdisj  5510  f00  5517  f0rn0  5520  f1rn  5532  f1ff1  5539  fimacnv  5764  ffvelcdm  5768  f1ompt  5786  fnfvrnss  5795  rnmptss  5796  fliftrel  5916  fo1stresm  6307  fo2ndresm  6308  1stcof  6309  2ndcof  6310  fo2ndf  6373  tposf2  6414  iunon  6430  smores2  6440  map0b  6834  mapsn  6837  f1imaen2g  6945  phplem4dom  7023  isinfinf  7059  updjudhcoinlf  7247  updjudhcoinrg  7248  casef  7255  unirnioo  10169  frecuzrdgdomlem  10639  frecuzrdgfunlem  10641  frecuzrdgtclt  10643  ennnfonelemrn  12990  ctinf  13001  txuni2  14930  blin2  15106  tgqioo  15229  reeff1o  15447  usgredgssen  15960