Theorem frn 5545

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 5384	. 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 4777   Fn wfn 5375   -->wf 5376

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 5384

This theorem is used by:  frnd  5546  fimass  5553  fco2  5557  fssxp  5558  fimacnvdisj  5579  f00  5587  f0rn0  5590  f1rn  5602  f1ff1  5609  fimacnv  5840  ffvelcdm  5844  f1ompt  5862  fnfvrnss  5871  rnmptss  5872  fliftrel  6001  fo1stresm  6399  fo2ndresm  6400  1stcof  6401  2ndcof  6402  fo2ndf  6467  tposf2  6544  iunon  6560  smores2  6570  map0b  6973  mapsnd  6976  mapsn  6978  f1imaen2g  7086  phplem4dom  7169  isinfinf  7207  updjudhcoinlf  7426  updjudhcoinrg  7427  casef  7434  unirnioo  10391  frecuzrdgdomlem  10874  frecuzrdgfunlem  10876  frecuzrdgtclt  10878  ballotfilemsima  13316  ennnfonelemrn  13367  ctinf  13378  txuni2  15499  blin2  15675  tgqioo  15798  reeff1o  16016  usgredgssen  16625