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

Theorem frn 5395
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 5259 . 2  |-  ( F : A --> B  <->  ( F  Fn  A  /\  ran  F  C_  B ) )
21simprbi 450 1  |-  ( F : A --> B  ->  ran  F  C_  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    C_ wss 3152   ran crn 4690    Fn wfn 5250   -->wf 5251
This theorem is referenced by:  fco2  5399  fssxp  5400  fimacnvdisj  5419  f00  5426  foconst  5462  fun11iun  5493  fimacnv  5657  ffvelrn  5663  f1ompt  5682  fnfvrnss  5687  f1dmex  5751  fliftrel  5807  isofr2  5841  fo1stres  6143  fo2ndres  6144  1stcof  6147  2ndcof  6148  fnwelem  6230  tposf2  6258  iunon  6355  iinon  6357  onoviun  6360  onnseq  6361  smores2  6371  seqomlem2  6463  oacomf1olem  6562  map0b  6806  mapsn  6809  f1imaen2g  6922  domdifsn  6945  domunsncan  6962  omxpenlem  6963  fodomr  7012  domss2  7020  f1finf1o  7086  f1fi  7143  unirnffid  7147  fissuni  7160  fipreima  7161  indexfi  7163  intrnfi  7170  dffi3  7184  ordtypelem8  7240  ordtypelem9  7241  ordtypelem10  7242  oismo  7255  hartogslem1  7257  brwdom2  7287  unxpwdom2  7302  ixpiunwdom  7305  infdifsn  7357  cantnf  7395  ac10ct  7661  numacn  7676  acndom  7678  acndom2  7681  infpwfien  7689  carduniima  7723  dfac12lem2  7770  dfac12lem3  7771  ackbij1  7864  fictb  7871  cfflb  7885  fin23lem40  7977  fin23lem41  7978  isf34lem5  8004  isf34lem7  8005  isf34lem6  8006  enfin1ai  8010  fin1a2lem6  8031  fin1a2lem7  8032  hsmexlem4  8055  hsmexlem5  8056  axdc2lem  8074  axdc3lem2  8077  ttukeylem6  8141  unirnfdomd  8189  pwcfsdom  8205  smobeth  8208  canthp1lem2  8275  pwfseqlem5  8285  wuncval2  8369  tskurn  8411  wfgru  8438  peano5nni  9749  rpnnen1lem4  10345  rpnnen1lem5  10346  unirnioo  10743  fseqsupcl  11039  fseqsupubi  11040  hashf1lem1  11393  hashf1lem2  11394  limsupcl  11947  limsupgle  11951  limsuple  11952  limsupval2  11954  limsupgre  11955  isercolllem2  12139  isercoll  12141  isercoll2  12142  climsup  12143  ruclem11  12518  prmreclem6  12968  4sqlem11  13002  vdwapf  13019  vdwlem11  13038  0ram  13067  0ram2  13068  0ramcl  13070  imasdsval2  13419  mrcssv  13516  isacs1i  13559  funcres2b  13771  funcres2c  13775  setcepi  13920  yoniso  14059  isacs4lem  14271  acsmapd  14281  acsmap2d  14282  mhmima  14440  gsumval1  14456  gsumwspan  14468  frmdss2  14485  cycsubgcl  14643  cycsubgss  14644  ghmrn  14696  conjnmz  14716  cntzmhm  14814  dfod2  14877  odcl2  14878  odf1o2  14884  sylow1lem2  14910  pgpssslw  14925  sylow2blem1  14931  lsmssv  14954  lsmidm  14973  pj1ghm2  15013  efgsp1  15046  efgsfo  15048  efgrelexlemb  15059  gexex  15145  iscyggen2  15168  cyggenod  15171  iscyg3  15173  gsumval3eu  15190  gsumval3  15191  cntzcmnf  15192  gsumzsubmcl  15200  gsumzaddlem  15203  gsumzadd  15204  gsumzsplit  15206  gsumconst  15209  gsumzoppg  15216  gsumpt  15222  dmdprdd  15237  dprdfcntz  15250  dprdfeq0  15257  dprdlub  15261  dprdres  15263  dprdss  15264  dprdz  15265  dprdf1  15268  subgdmdprd  15269  subgdprd  15270  dprd2dlem1  15276  dprd2da  15277  dmdprdsplit2lem  15280  dpjghm2  15299  ablfac1b  15305  lmhmlsp  15806  pj1lmhm2  15854  aspval2  16086  mplbas2  16212  mplind  16243  pjfo  16615  iinopn  16648  tgiun  16717  pptbas  16745  tgrest  16890  resttopon  16892  rest0  16900  restfpw  16910  ordtbaslem  16918  ordtuni  16920  ordtbas2  16921  ordtrest  16932  ordtrest2  16934  leordtval2  16942  lecldbas  16949  cnclsi  17001  cnrest  17013  cnrest2r  17015  cnprest2  17018  lmss  17026  cncmp  17119  rncmp  17123  discmp  17125  cmpsub  17127  tgcmp  17128  hauscmplem  17133  conima  17151  concn  17152  2ndcctbss  17181  2ndcdisj  17182  2ndcomap  17184  2ndcsep  17185  dis2ndc  17186  lly1stc  17222  kgentop  17237  kgencmp  17240  1stckgenlem  17248  1stckgen  17249  kgencn2  17252  kgencn3  17253  txuni2  17260  ptbasfi  17276  xkoopn  17284  xkouni  17294  txbasval  17301  xkoccn  17313  ptcnplem  17315  upxp  17317  uptx  17319  txtube  17334  txcmplem1  17335  txcmplem2  17336  tx1stc  17344  txkgen  17346  xkoptsub  17348  xkoco1cn  17351  xkoco2cn  17352  xkococnlem  17353  xkococn  17354  xkoinjcn  17381  hmeores  17462  hmphdis  17487  fbasrn  17579  trfilss  17584  trfg  17586  zfbas  17591  uzrest  17592  elfm  17642  imaelfm  17646  rnelfmlem  17647  fclscmpi  17724  alexsublem  17738  alexsubALT  17745  ptcmplem1  17746  ptcmplem3  17748  tmdgsum2  17779  symgtgp  17784  submtmd  17787  subgtgp  17788  subgntr  17789  opnsubg  17790  clsnsg  17792  tgpconcomp  17795  tsmsfbas  17810  tsmsxplem1  17835  prdsdsf  17931  prdsxmetlem  17932  prdsmet  17934  imasdsf1olem  17937  unirnbl  17969  blin2  17975  imasf1oxms  18035  prdsbl  18037  met1stc  18067  met2ndci  18068  prdsxmslem2  18075  tgqioo  18306  xrtgioo  18312  xrge0gsumle  18338  xrge0tsms  18339  metdcn2  18344  metdsf  18352  metdsge  18353  metdscn2  18361  cnmptre  18425  iimulcn  18436  icchmeo  18439  xrhmeo  18444  cnheiborlem  18452  bndth  18456  evth  18457  evth2  18458  lebnumlem2  18460  lebnumlem3  18461  reparphti  18495  tchex  18649  tchnmfval  18659  fmcfil  18698  causs  18724  bcthlem5  18750  minveclem1  18788  minveclem3b  18792  evthicc2  18820  ovolficcss  18829  elovolm  18834  ovolmge0  18836  ovollb  18838  ovolgelb  18839  ovollb2lem  18847  ovollb2  18848  ovolunlem1a  18855  ovolunlem1  18856  ovoliunlem1  18861  ovoliunlem2  18862  ovoliun  18864  ovoliun2  18865  ovolscalem1  18872  ovolicc1  18875  ovolicc2lem4  18879  ovolicc2  18881  voliunlem2  18908  voliunlem3  18909  volsup  18913  ioombl1lem2  18916  ioombl1lem4  18918  uniioovol  18934  uniiccvol  18935  uniioombllem1  18936  uniioombllem2  18938  uniioombllem3  18940  uniioombllem6  18943  uniioombl  18944  dyadmbllem  18954  dyadmbl  18955  opnmbllem  18956  opnmblALT  18958  volsup2  18960  vitalilem2  18964  vitalilem4  18966  vitalilem5  18967  mbfconstlem  18984  mbfsup  19019  mbfinf  19020  mbflimsup  19021  i1fima  19033  i1fima2  19034  i1fd  19036  itg1cl  19040  itg1ge0  19041  i1f1  19045  itg11  19046  i1fmullem  19049  i1fadd  19050  i1fmul  19051  itg1addlem4  19054  itg1addlem5  19055  i1fmulc  19058  itg1mulc  19059  i1fres  19060  itg10a  19065  itg1ge0a  19066  itg1climres  19069  mbfi1fseqlem4  19073  itg2seq  19097  itg2monolem1  19105  itg2monolem2  19106  itg2monolem3  19107  itg2mono  19108  itg2i1fseq2  19111  itg2gt0  19115  itg2cnlem1  19116  itg2cn  19118  limciun  19244  c1liplem1  19343  dvne0  19358  dvne0f1  19359  lhop2  19362  dvcnvrelem2  19365  dvcnvre  19366  evlslem1  19399  evlseu  19400  mdegleb  19450  mdeglt  19451  mdegldg  19452  mdegxrcl  19453  mdegcl  19455  ig1peu  19557  aalioulem3  19714  ulmss  19774  reeff1o  19823  efifo  19909  dvlog  19998  efopn  20005  logccv  20010  efrlim  20264  basellem3  20320  fsumvma  20452  lgseisenlem4  20591  dchrisum0fno1  20660  ghsubgolem  21037  ubthlem1  21449  minvecolem1  21453  htthlem  21497  hhssims  21852  shsss  21892  pjrni  22281  imaelshi  22638  ballotlemsima  23074  ofrn  23206  ofrn2  23207  xppreima2  23212  rnmptss  23238  xrge0mulc1cn  23323  rge0scvg  23373  xrge0tsmsd  23382  esumcst  23436  esumpfinvallem  23442  esumpcvgval  23446  esumcvg  23454  rrvrnss  23650  orvcval4  23661  erdsze2lem2  23735  cvxpcon  23773  cvxscon  23774  cvmsss2  23805  cvmliftlem8  23823  cvmlift3lem6  23855  ghomgrpilem2  23993  ghomfo  23998  orderseqlem  24252  norn  24305  basexre  25522  cmptdst  25568  limptlimpr2lem2  25575  bwt2  25592  supnuf  25629  supbrr  25636  rdmob  25748  rcmob  25749  comppfsc  26307  neibastop2lem  26309  tailfb  26326  indexdom  26413  cnresima  26484  istotbnd3  26495  sstotbnd2  26498  sstotbnd  26499  totbndbnd  26513  prdsbnd  26517  cntotbnd  26520  ismtyima  26527  heibor1lem  26533  heiborlem1  26535  heibor  26545  rrnval  26551  rrnequiv  26559  reheibor  26563  elrfirn  26770  cmpfiiin  26772  isnacs2  26781  isnacs3  26785  nacsfix  26787  coeq0i  26832  diophrw  26838  eldioph2lem2  26840  dnwech  27145  fnwe2lem2  27148  lmhmfgima  27182  pwssplit4  27191  frlmsplit2  27243  frlmsslsp  27248  frlmlbs  27249  frlmup3  27252  frlmup4  27253  lindff1  27290  lindfrn  27291  f1lindf  27292  lindfmm  27297  indlcim  27310  hbt  27334  f1omvdconj  27389  psgnunilem1  27416  fnvinran  27685  refsumcn  27701  cncmpmax  27703  climinf  27732  fafvelrn  28032  lsatset  29180  lsatlss  29186  cdleme50rnlem  30733
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360  df-f 5259
  Copyright terms: Public domain W3C validator