MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  frn Structured version   Unicode version

Theorem frn 5600
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
StepHypRef Expression
1 df-f 5461 . 2  |-  ( F : A --> B  <->  ( F  Fn  A  /\  ran  F  C_  B ) )
21simprbi 452 1  |-  ( F : A --> B  ->  ran  F  C_  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    C_ wss 3322   ran crn 4882    Fn wfn 5452   -->wf 5453
This theorem is referenced by:  fco2  5604  fssxp  5605  fimacnvdisj  5624  f00  5631  foconst  5667  fun11iun  5698  fimacnv  5865  ffvelrn  5871  f1ompt  5894  fnfvrnss  5899  rnmptss  5900  f1dmex  5974  fliftrel  6033  isofr2  6067  fo1stres  6373  fo2ndres  6374  1stcof  6377  2ndcof  6378  fo2ndf  6456  fnwelem  6464  tposf2  6506  iunon  6603  iinon  6605  onoviun  6608  onnseq  6609  smores2  6619  seqomlem2  6711  oacomf1olem  6810  map0b  7055  mapsn  7058  f1imaen2g  7171  domdifsn  7194  domunsncan  7211  omxpenlem  7212  fodomr  7261  domss2  7269  f1finf1o  7338  f1fi  7396  unirnffid  7401  fissuni  7414  fipreima  7415  indexfi  7417  intrnfi  7424  dffi3  7439  ordtypelem8  7497  ordtypelem9  7498  ordtypelem10  7499  oismo  7512  hartogslem1  7514  brwdom2  7544  unxpwdom2  7559  ixpiunwdom  7562  infdifsn  7614  cantnf  7652  ac10ct  7920  numacn  7935  acndom  7937  acndom2  7940  infpwfien  7948  carduniima  7982  dfac12lem2  8029  dfac12lem3  8030  ackbij1  8123  fictb  8130  cfflb  8144  fin23lem40  8236  fin23lem41  8237  isf34lem5  8263  isf34lem7  8264  isf34lem6  8265  enfin1ai  8269  fin1a2lem6  8290  fin1a2lem7  8291  hsmexlem4  8314  hsmexlem5  8315  axdc2lem  8333  axdc3lem2  8336  ttukeylem6  8399  unirnfdomd  8447  pwcfsdom  8463  smobeth  8466  canthp1lem2  8533  pwfseqlem5  8543  wuncval2  8627  tskurn  8669  wfgru  8696  peano5nni  10008  rpnnen1lem4  10608  rpnnen1lem5  10609  unirnioo  11009  fseqsupcl  11321  fseqsupubi  11322  hashf1lem1  11709  hashf1lem2  11710  limsupcl  12272  limsupgle  12276  limsuple  12277  limsupval2  12279  limsupgre  12280  isercolllem2  12464  isercoll  12466  isercoll2  12467  climsup  12468  ruclem11  12844  prmreclem6  13294  4sqlem11  13328  vdwapf  13345  vdwlem11  13364  0ram  13393  0ram2  13394  0ramcl  13396  imasdsval2  13747  mrcssv  13844  isacs1i  13887  funcres2b  14099  funcres2c  14103  setcepi  14248  yoniso  14387  isacs4lem  14599  acsmapd  14609  acsmap2d  14610  mhmima  14768  gsumval1  14784  gsumwspan  14796  frmdss2  14813  cycsubgcl  14971  cycsubgss  14972  ghmrn  15024  conjnmz  15044  cntzmhm  15142  dfod2  15205  odcl2  15206  odf1o2  15212  sylow1lem2  15238  pgpssslw  15253  sylow2blem1  15259  lsmssv  15282  lsmidm  15301  pj1ghm2  15341  efgsp1  15374  efgsfo  15376  efgrelexlemb  15387  gexex  15473  iscyggen2  15496  cyggenod  15499  iscyg3  15501  gsumval3eu  15518  gsumval3  15519  cntzcmnf  15520  gsumzsubmcl  15528  gsumzaddlem  15531  gsumzadd  15532  gsumzsplit  15534  gsumconst  15537  gsumzoppg  15544  gsumpt  15550  dmdprdd  15565  dprdfcntz  15578  dprdfeq0  15585  dprdlub  15589  dprdres  15591  dprdss  15592  dprdz  15593  dprdf1  15596  subgdmdprd  15597  subgdprd  15598  dprd2dlem1  15604  dprd2da  15605  dmdprdsplit2lem  15608  dpjghm2  15627  ablfac1b  15633  lmhmlsp  16130  pj1lmhm2  16178  aspval2  16410  mplbas2  16536  mplind  16567  pjfo  16947  iinopn  16980  tgiun  17049  pptbas  17077  tgrest  17228  resttopon  17230  rest0  17238  restfpw  17248  ordtbaslem  17257  ordtuni  17259  ordtbas2  17260  ordtrest  17271  ordtrest2  17273  leordtval2  17281  lecldbas  17288  cnclsi  17341  cnrest  17354  cnrest2r  17356  cnprest2  17359  lmss  17367  cncmp  17460  rncmp  17464  discmp  17466  cmpsub  17468  tgcmp  17469  hauscmplem  17474  bwth  17478  conima  17493  concn  17494  2ndcctbss  17523  2ndcdisj  17524  2ndcomap  17526  2ndcsep  17527  dis2ndc  17528  lly1stc  17564  kgentop  17579  kgencmp  17582  1stckgenlem  17590  1stckgen  17591  kgencn2  17594  kgencn3  17595  txuni2  17602  ptbasfi  17618  xkoopn  17626  xkouni  17636  txbasval  17643  xkoccn  17656  ptcnplem  17658  upxp  17660  uptx  17662  txtube  17677  txcmplem1  17678  txcmplem2  17679  tx1stc  17687  txkgen  17689  xkoptsub  17691  xkoco1cn  17694  xkoco2cn  17695  xkococnlem  17696  xkococn  17697  xkoinjcn  17724  hmeores  17808  hmphdis  17833  fbasrn  17921  trfilss  17926  trfg  17928  zfbas  17933  uzrest  17934  elfm  17984  imaelfm  17988  rnelfmlem  17989  fclscmpi  18066  alexsublem  18080  alexsubALT  18087  ptcmplem1  18088  ptcmplem3  18090  cnextcn  18103  tmdgsum2  18131  symgtgp  18136  submtmd  18139  subgtgp  18140  subgntr  18141  opnsubg  18142  clsnsg  18144  tgpconcomp  18147  tsmsfbas  18162  tsmsxplem1  18187  prdsdsf  18402  prdsxmetlem  18403  prdsmet  18405  imasdsf1olem  18408  unirnblps  18454  unirnbl  18455  blin2  18464  imasf1oxms  18524  prdsbl  18526  met1stc  18556  met2ndci  18557  prdsxmslem2  18564  tgqioo  18836  xrtgioo  18842  xrge0gsumle  18869  xrge0tsms  18870  metdcn2  18875  metdsf  18883  metdsge  18884  metdscn2  18892  cnmptre  18957  iimulcn  18968  icchmeo  18971  xrhmeo  18976  cnheiborlem  18984  bndth  18988  evth  18989  evth2  18990  lebnumlem2  18992  lebnumlem3  18993  reparphti  19027  tchex  19181  tchnmfval  19191  fmcfil  19230  causs  19256  bcthlem5  19286  minveclem1  19330  minveclem3b  19334  evthicc2  19362  ovolficcss  19371  elovolm  19376  ovolmge0  19378  ovollb  19380  ovolgelb  19381  ovollb2lem  19389  ovollb2  19390  ovolunlem1a  19397  ovolunlem1  19398  ovoliunlem1  19403  ovoliunlem2  19404  ovoliun  19406  ovoliun2  19407  ovolscalem1  19414  ovolicc1  19417  ovolicc2lem4  19421  ovolicc2  19423  voliunlem2  19450  voliunlem3  19451  volsup  19455  ioombl1lem2  19458  ioombl1lem4  19460  uniioovol  19476  uniiccvol  19477  uniioombllem1  19478  uniioombllem2  19480  uniioombllem3  19482  uniioombllem6  19485  uniioombl  19486  dyadmbllem  19496  dyadmbl  19497  opnmbllem  19498  opnmblALT  19500  volsup2  19502  vitalilem2  19506  vitalilem4  19508  vitalilem5  19509  mbfconstlem  19524  mbfsup  19559  mbfinf  19560  mbflimsup  19561  i1fima  19573  i1fima2  19574  i1fd  19576  itg1cl  19580  itg1ge0  19581  i1f1  19585  itg11  19586  i1fmullem  19589  i1fadd  19590  i1fmul  19591  itg1addlem4  19594  itg1addlem5  19595  i1fmulc  19598  itg1mulc  19599  i1fres  19600  itg10a  19605  itg1ge0a  19606  itg1climres  19609  mbfi1fseqlem4  19613  itg2seq  19637  itg2monolem1  19645  itg2monolem2  19646  itg2monolem3  19647  itg2mono  19648  itg2i1fseq2  19651  itg2gt0  19655  itg2cnlem1  19656  itg2cn  19658  limciun  19786  c1liplem1  19885  dvne0  19900  dvne0f1  19901  lhop2  19904  dvcnvrelem2  19907  dvcnvre  19908  evlslem1  19941  evlseu  19942  mdegleb  19992  mdeglt  19993  mdegldg  19994  mdegxrcl  19995  mdegcl  19997  ig1peu  20099  aalioulem3  20256  ulmss  20318  reeff1o  20368  efifo  20454  dvlog  20547  efopn  20554  logccv  20559  efrlim  20813  basellem3  20870  fsumvma  21002  lgseisenlem4  21141  dchrisum0fno1  21210  ghsubgolem  21963  ubthlem1  22377  minvecolem1  22381  htthlem  22425  hhssims  22780  shsss  22820  pjrni  23209  imaelshi  23566  ofrn  24057  ofrn2  24058  xppreima2  24065  xrge0tsmsd  24228  xrge0mulc1cn  24332  rge0scvg  24340  esumcst  24460  esumpfinvallem  24469  esumpcvgval  24473  esumcvg  24481  sitgclg  24661  sitgclbn  24662  rrvrnss  24710  orvcval4  24723  ballotlemsima  24778  lgamcvg2  24844  erdsze2lem2  24895  cvxpcon  24934  cvxscon  24935  cvmsss2  24966  cvmliftlem8  24984  cvmlift3lem6  25016  ghomgrpilem2  25102  ghomfo  25107  orderseqlem  25532  norn  25611  heicant  26253  opnmbllem0  26254  mblfinlem1  26255  mblfinlem2  26256  mblfinlem3  26257  mblfinlem4  26258  ismblfin  26259  volsupnfl  26263  itg2addnclem2  26271  itg2gt0cn  26274  ftc1anclem3  26296  ftc1anclem5  26298  ftc1anclem6  26299  ftc1anclem7  26300  ftc1anclem8  26301  ftc1anc  26302  comppfsc  26401  neibastop2lem  26403  tailfb  26420  indexdom  26450  cnresima  26487  istotbnd3  26494  sstotbnd2  26497  sstotbnd  26498  totbndbnd  26512  prdsbnd  26516  cntotbnd  26519  ismtyima  26526  heibor1lem  26532  heiborlem1  26534  heibor  26544  rrnval  26550  rrnequiv  26558  reheibor  26562  elrfirn  26763  cmpfiiin  26765  isnacs2  26774  isnacs3  26778  nacsfix  26780  coeq0i  26825  diophrw  26831  eldioph2lem2  26833  dnwech  27137  fnwe2lem2  27140  lmhmfgima  27173  pwssplit4  27182  frlmsplit2  27234  frlmsslsp  27239  frlmlbs  27240  frlmup3  27243  frlmup4  27244  lindff1  27281  lindfrn  27282  f1lindf  27283  lindfmm  27288  indlcim  27301  hbt  27325  f1omvdconj  27380  psgnunilem1  27407  refsumcn  27691  cncmpmax  27693  climinf  27722  fafvelrn  28024  f0rn0  28093  hashimarn  28186  frgrancvvdeqlem8  28503  lsatset  29862  lsatlss  29868  cdleme50rnlem  31415
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 179  df-an 362  df-f 5461
  Copyright terms: Public domain W3C validator