Theorem frn 6053

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

Syntax hints:   -> wi 4   C_ wss 3574   ran crn 5115   Fn wfn 5883   -->wf 5884

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 386  df-f 5892

This theorem is referenced by:  fco2  6059  fssxp  6060  fimass  6081  fimacnvdisj  6083  f00  6087  f0rn0  6090  foconst  6126  fimacnv  6347  ffvelrn  6357  f1ompt  6382  fnfvrnss  6390  rnmptss  6392  fliftrel  6558  isofr2  6594  fun11iun  7126  f1dmex  7136  fo1stres  7192  fo2ndres  7193  1stcof  7196  2ndcof  7197  fo2ndf  7284  fnwelem  7292  tposf2  7376  onoviun  7440  onnseq  7441  smores2  7451  seqomlem2  7546  oacomf1olem  7644  map0b  7896  mapsn  7899  f1imaen2g  8017  domdifsn  8043  domunsncan  8060  omxpenlem  8061  fodomr  8111  domss2  8119  f1finf1o  8187  f1fi  8253  unirnffid  8258  fipreima  8272  indexfi  8274  intrnfi  8322  dffi3  8337  ordtypelem8  8430  ordtypelem9  8431  ordtypelem10  8432  oismo  8445  hartogslem1  8447  brwdom2  8478  unxpwdom2  8493  ixpiunwdom  8496  infdifsn  8554  cantnf  8590  ac10ct  8857  numacn  8872  acndom  8874  acndom2  8877  infpwfien  8885  carduniima  8919  dfac12lem2  8966  dfac12lem3  8967  ackbij1  9060  fictb  9067  cfflb  9081  fin23lem40  9173  fin23lem41  9174  isf34lem5  9200  isf34lem7  9201  isf34lem6  9202  enfin1ai  9206  fin1a2lem6  9227  fin1a2lem7  9228  hsmexlem4  9251  hsmexlem5  9252  axdc2lem  9270  axdc3lem2  9273  ttukeylem6  9336  unirnfdomd  9389  pwcfsdom  9405  smobeth  9408  canthp1lem2  9475  pwfseqlem5  9485  wuncval2  9569  tskurn  9611  wfgru  9638  peano5nni  11023  rpnnen1lem4  11817  rpnnen1lem5  11818  rpnnen1lem4OLD  11823  rpnnen1lem5OLD  11824  unirnioo  12273  fseqsupcl  12776  fseqsupubi  12777  hashimarn  13227  hashf1lem1  13239  hashf1lem2  13240  ccatrn  13372  swrdrn  13429  cshwrn  13548  limsupcl  14204  limsupgle  14208  limsuple  14209  limsupval2  14211  limsupgre  14212  isercolllem2  14396  isercoll  14398  isercoll2  14399  climsup  14400  ruclem11  14969  prmreclem6  15625  4sqlem11  15659  vdwapf  15676  vdwlem11  15695  0ram  15724  0ram2  15725  0ramcl  15727  imasdsval2  16176  mrcssv  16274  isacs1i  16318  funcres2b  16557  funcres2c  16561  setcepi  16738  yoniso  16925  isacs4lem  17168  acsmapd  17178  acsmap2d  17179  gsumval1  17277  mhmima  17363  gsumwspan  17383  frmdss2  17400  cycsubgcl  17620  cycsubgss  17621  ghmrn  17673  conjnmz  17694  cntzmhm  17771  f1omvdconj  17866  psgnunilem1  17913  dfod2  17981  odcl2  17982  odf1o2  17988  sylow1lem2  18014  pgpssslw  18029  sylow2blem1  18035  lsmssv  18058  lsmidm  18077  pj1ghm2  18117  efgsp1  18150  efgsfo  18152  efgrelexlemb  18163  cntzcmnf  18248  gexex  18256  iscyggen2  18283  cyggenod  18286  iscyg3  18288  gsumval3eu  18305  gsumval3lem1  18306  gsumval3lem2  18307  gsumval3  18308  gsumzsubmcl  18318  gsumzaddlem  18321  gsumzadd  18322  gsumzsplit  18327  gsumconst  18334  gsumzoppg  18344  gsumpt  18361  dmdprdd  18398  dprdfcntz  18414  dprdfeq0  18421  dprdlub  18425  dprdres  18427  dprdss  18428  dprdz  18429  dprdf1  18432  subgdmdprd  18433  subgdprd  18434  dprd2dlem1  18440  dprd2da  18441  dmdprdsplit2lem  18444  dpjghm2  18463  ablfac1b  18469  lmhmlsp  19049  pj1lmhm2  19101  aspval2  19347  mplcoe5lem  19467  mplbas2  19470  mplind  19502  evlslem1  19515  evlseu  19516  gsumply1subr  19604  pjfo  20059  frlmsplit2  20112  frlmsslsp  20135  frlmlbs  20136  frlmup3  20139  frlmup4  20140  lindff1  20159  lindfrn  20160  f1lindf  20161  lindfmm  20166  indlcim  20179  m2cpmf1  20548  m2cpmghm  20549  m2cpmmhm  20550  iinopn  20707  pptbas  20812  tgrest  20963  resttopon  20965  rest0  20973  restfpw  20983  ordtbaslem  20992  ordtuni  20994  ordtbas2  20995  ordtrest  21006  ordtrest2  21008  leordtval2  21016  lecldbas  21023  cnclsi  21076  cnrest2r  21091  cnprest2  21094  lmss  21102  cncmp  21195  rncmp  21199  discmp  21201  cmpsub  21203  tgcmp  21204  hauscmplem  21209  connima  21228  conncn  21229  2ndcctbss  21258  2ndcdisj  21259  2ndcomap  21261  2ndcsep  21262  dis2ndc  21263  lly1stc  21299  comppfsc  21335  kgentop  21345  kgencmp  21348  1stckgenlem  21356  1stckgen  21357  kgencn2  21360  kgencn3  21361  txuni2  21368  ptbasfi  21384  xkoopn  21392  xkouni  21402  txbasval  21409  xkoccn  21422  ptcnplem  21424  upxp  21426  uptx  21428  txtube  21443  txcmplem1  21444  txcmplem2  21445  tx1stc  21453  txkgen  21455  xkoptsub  21457  xkoco1cn  21460  xkoco2cn  21461  xkococnlem  21462  xkococn  21463  xkoinjcn  21490  hmeores  21574  hmphdis  21599  fbasrn  21688  trfilss  21693  trfg  21695  zfbas  21700  uzrest  21701  elfm  21751  imaelfm  21755  rnelfmlem  21756  fclscmpi  21833  alexsublem  21848  alexsubALT  21855  ptcmplem1  21856  ptcmplem3  21858  cnextcn  21871  tmdgsum2  21900  symgtgp  21905  submtmd  21908  subgtgp  21909  subgntr  21910  opnsubg  21911  clsnsg  21913  tgpconncomp  21916  tsmsfbas  21931  tsmsxplem1  21956  prdsdsf  22172  prdsxmetlem  22173  prdsmet  22175  imasdsf1olem  22178  unirnblps  22224  unirnbl  22225  blin2  22234  imasf1oxms  22294  prdsbl  22296  met1stc  22326  met2ndci  22327  prdsxmslem2  22334  tgqioo  22603  xrtgioo  22609  xrge0gsumle  22636  xrge0tsms  22637  metdcn2  22642  metdsf  22651  metdsge  22652  metdscn2  22660  cnmptre  22726  iimulcn  22737  icchmeo  22740  xrhmeo  22745  cnheiborlem  22753  bndth  22757  evth  22758  evth2  22759  lebnumlem2  22761  lebnumlem3  22762  reparphti  22797  tchex  23016  tchnmfval  23027  fmcfil  23070  causs  23096  bcthlem5  23125  minveclem1  23195  minveclem3b  23199  evthicc2  23229  ovolficcss  23238  elovolm  23243  ovolmge0  23245  ovollb  23247  ovolgelb  23248  ovollb2lem  23256  ovollb2  23257  ovolunlem1a  23264  ovolunlem1  23265  ovoliunlem1  23270  ovoliunlem2  23271  ovoliun  23273  ovoliun2  23274  ovolscalem1  23281  ovolicc1  23284  ovolicc2lem4  23288  ovolicc2  23290  voliunlem2  23319  voliunlem3  23320  volsup  23324  ioombl1lem2  23327  ioombl1lem4  23329  uniioovol  23347  uniiccvol  23348  uniioombllem1  23349  uniioombllem2  23351  uniioombllem3  23353  uniioombllem6  23356  uniioombl  23357  dyadmbllem  23367  dyadmbl  23368  opnmbllem  23369  opnmblALT  23371  volsup2  23373  vitalilem2  23378  vitalilem4  23380  vitalilem5  23381  mbfconstlem  23396  mbfsup  23431  mbfinf  23432  mbflimsup  23433  i1fima  23445  i1fima2  23446  i1fd  23448  itg1cl  23452  itg1ge0  23453  i1f1  23457  itg11  23458  i1fmullem  23461  i1fadd  23462  i1fmul  23463  itg1addlem4  23466  itg1addlem5  23467  i1fmulc  23470  itg1mulc  23471  i1fres  23472  itg10a  23477  itg1ge0a  23478  itg1climres  23481  mbfi1fseqlem4  23485  itg2seq  23509  itg2monolem1  23517  itg2monolem2  23518  itg2monolem3  23519  itg2mono  23520  itg2i1fseq2  23523  itg2gt0  23527  itg2cnlem1  23528  itg2cn  23530  limciun  23658  c1liplem1  23759  dvne0  23774  dvne0f1  23775  lhop2  23778  dvcnvrelem2  23781  dvcnvre  23782  mdegleb  23824  mdeglt  23825  mdegldg  23826  mdegxrcl  23827  mdegcl  23829  ig1peu  23931  aalioulem3  24089  ulmss  24151  reeff1o  24201  efifo  24293  dvlog  24397  efopn  24404  logccv  24409  efrlim  24696  lgamcvg2  24781  basellem3  24809  fsumvma  24938  lgseisenlem4  25103  dchrisum0fno1  25200  uhgredgn0  26023  upgredgss  26027  umgredgss  26028  edgupgr  26029  upgredg  26032  usgredgss  26054  usgruspgrb  26076  upgrres1  26205  ubthlem1  27726  minvecolem1  27730  htthlem  27774  hhssims  28132  shsss  28172  pjrni  28561  imaelshi  28917  foresf1o  29343  ofrn  29441  ofrn2  29442  fimarab  29445  xppreima2  29450  fsumiunle  29575  xrge0tsmsd  29785  smatrcl  29862  locfinreflem  29907  cmpcref  29917  ordtrestNEW  29967  ordtrest2NEW  29969  xrge0mulc1cn  29987  rge0scvg  29995  esumcst  30125  esumpfinvallem  30136  esumpcvgval  30140  esumcvg  30148  esumiun  30156  omssubadd  30362  carsggect  30380  sibfinima  30401  sitgclg  30404  sitgclbn  30405  sitgaddlemb  30410  eulerpartgbij  30434  eulerpartlemgvv  30438  eulerpartlemgf  30441  rrvrnss  30509  orvcval4  30522  ballotlemsima  30577  erdsze2lem2  31186  cvxpconn  31224  cvxsconn  31225  cvmsss2  31256  cvmliftlem8  31274  cvmlift3lem6  31306  mrsubrn  31410  mrsubf  31414  msubrn  31426  msubf  31429  mstapst  31444  mvtss  31450  mclsssvlem  31459  mclsax  31466  mclsind  31467  mclsppslem  31480  orderseqlem  31749  norn  31804  neibastop2lem  32355  tailfb  32372  knoppcnlem10  32492  icoreunrn  33207  lindsdom  33403  ptrecube  33409  poimirlem1  33410  poimirlem2  33411  poimirlem3  33412  poimirlem11  33420  poimirlem12  33421  poimirlem16  33425  poimirlem19  33428  poimirlem27  33436  poimirlem30  33439  poimirlem32  33441  broucube  33443  heicant  33444  opnmbllem0  33445  mblfinlem1  33446  mblfinlem2  33447  mblfinlem3  33448  mblfinlem4  33449  ismblfin  33450  volsupnfl  33454  itg2addnclem2  33462  itg2gt0cn  33465  ftc1anclem3  33487  ftc1anclem5  33489  ftc1anclem6  33490  ftc1anclem7  33491  ftc1anclem8  33492  ftc1anc  33493  indexdom  33529  cnresima  33563  istotbnd3  33570  sstotbnd2  33573  sstotbnd  33574  totbndbnd  33588  prdsbnd  33592  cntotbnd  33595  ismtyima  33602  heibor1lem  33608  heiborlem1  33610  heibor  33620  rrnval  33626  rrnequiv  33634  reheibor  33638  lsatset  34277  lsatlss  34283  cdleme50rnlem  35832  elrfirn  37258  cmpfiiin  37260  isnacs2  37269  isnacs3  37273  nacsfix  37275  coeq0i  37316  diophrw  37322  eldioph2lem2  37324  dnwech  37618  fnwe2lem2  37621  lmhmfgima  37654  pwssplit4  37659  hbt  37700  imo72b2lem0  38465  imo72b2lem2  38467  imo72b2lem1  38471  imo72b2  38475  refsumcn  39189  cncmpmax  39191  mapsnd  39388  elpmrn  39414  frnd  39426  rnmptssf  39462  climinf  39838  liminfval2  40000  icccncfext  40100  dvsinax  40127  itgsubsticclem  40191  fourierdlem12  40336  fourierdlem42  40366  fourierdlem54  40377  fourierdlem70  40393  fourierdlem76  40399  fourierdlem82  40405  fourierdlem85  40408  fourierdlem88  40411  fourierdlem93  40416  fourierdlem113  40436  fge0npnf  40584  sge0resrnlem  40620  sge0isum  40644  sge0seq  40663  meadjiunlem  40682  omeiunle  40731  hoicvr  40762  vonvolmbllem  40874  vonvolmbl2  40877  vonvol2  40878  fafvelrn  41250  pfxrn  41393  mgmplusfreseq  41773  mgmhmima  41802  elbigolo1  42351  aacllem  42547