Theorem frn 5375

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 5221	. 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 3130   ran crn 4628   Fn wfn 5212   -->wf 5213

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 5221

This theorem is referenced by:  frnd  5376  fco2  5383  fssxp  5384  fimacnvdisj  5401  f00  5408  f0rn0  5411  f1rn  5423  f1ff1  5430  fimacnv  5646  ffvelcdm  5650  f1ompt  5668  fnfvrnss  5677  rnmptss  5678  fliftrel  5793  fo1stresm  6162  fo2ndresm  6163  1stcof  6164  2ndcof  6165  fo2ndf  6228  tposf2  6269  iunon  6285  smores2  6295  map0b  6687  mapsn  6690  f1imaen2g  6793  phplem4dom  6862  isinfinf  6897  updjudhcoinlf  7079  updjudhcoinrg  7080  casef  7087  unirnioo  9973  frecuzrdgdomlem  10417  frecuzrdgfunlem  10419  frecuzrdgtclt  10421  ennnfonelemrn  12420  ctinf  12431  txuni2  13759  blin2  13935  tgqioo  14050  reeff1o  14197