Theorem frn 5276

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

Syntax hints:   -> wi 4   C_ wss 3066   ran crn 4535   Fn wfn 5113   -->wf 5114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106

This theorem depends on definitions:  df-bi 116  df-f 5122

This theorem is referenced by:  frnd  5277  fco2  5284  fssxp  5285  fimacnvdisj  5302  f00  5309  f0rn0  5312  f1rn  5324  f1ff1  5331  fimacnv  5542  ffvelrn  5546  f1ompt  5564  fnfvrnss  5573  rnmptss  5574  fliftrel  5686  fo1stresm  6052  fo2ndresm  6053  1stcof  6054  2ndcof  6055  fo2ndf  6117  tposf2  6158  iunon  6174  smores2  6184  map0b  6574  mapsn  6577  f1imaen2g  6680  phplem4dom  6749  isinfinf  6784  updjudhcoinlf  6958  updjudhcoinrg  6959  casef  6966  unirnioo  9749  frecuzrdgdomlem  10183  frecuzrdgfunlem  10185  frecuzrdgtclt  10187  ennnfonelemrn  11921  ctinf  11932  txuni2  12414  blin2  12590  tgqioo  12705