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

Theorem frn 5553
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 5410 . 2  |-  ( F : A --> B  <->  ( F  Fn  A  /\  ran  F  C_  B ) )
21simprbi 461 1  |-  ( F : A --> B  ->  ran  F  C_  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    C_ wss 3316   ran crn 4828    Fn wfn 5401   -->wf 5402
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 185  df-an 371  df-f 5410
This theorem is referenced by:  fco2  5557  fssxp  5558  fimacnvdisj  5577  f00  5581  foconst  5619  fimacnv  5823  ffvelrn  5829  f1ompt  5853  fnfvrnss  5858  rnmptss  5859  fliftrel  5988  isofr2  6022  fun11iun  6526  f1dmex  6536  fo1stres  6589  fo2ndres  6590  1stcof  6593  2ndcof  6594  fo2ndf  6668  fnwelem  6676  tposf2  6758  iunon  6785  iinon  6787  onoviun  6790  onnseq  6791  smores2  6801  seqomlem2  6892  oacomf1olem  6991  map0b  7239  mapsn  7242  f1imaen2g  7358  domdifsn  7382  domunsncan  7399  omxpenlem  7400  fodomr  7450  domss2  7458  f1finf1o  7527  f1fi  7586  unirnffid  7591  fissuni  7604  fipreima  7605  indexfi  7607  intrnfi  7654  dffi3  7669  ordtypelem8  7727  ordtypelem9  7728  ordtypelem10  7729  oismo  7742  hartogslem1  7744  brwdom2  7776  unxpwdom2  7791  ixpiunwdom  7794  infdifsn  7850  cantnf  7889  cantnfOLD  7911  ac10ct  8192  numacn  8207  acndom  8209  acndom2  8212  infpwfien  8220  carduniima  8254  dfac12lem2  8301  dfac12lem3  8302  ackbij1  8395  fictb  8402  cfflb  8416  fin23lem40  8508  fin23lem41  8509  isf34lem5  8535  isf34lem7  8536  isf34lem6  8537  enfin1ai  8541  fin1a2lem6  8562  fin1a2lem7  8563  hsmexlem4  8586  hsmexlem5  8587  axdc2lem  8605  axdc3lem2  8608  ttukeylem6  8671  unirnfdomd  8719  pwcfsdom  8735  smobeth  8738  canthp1lem2  8807  pwfseqlem5  8817  wuncval2  8901  tskurn  8943  wfgru  8970  peano5nni  10312  rpnnen1lem4  10969  rpnnen1lem5  10970  unirnioo  11376  fseqsupcl  11782  fseqsupubi  11783  hashimarn  12183  hashf1lem1  12191  hashf1lem2  12192  swrdrn  12306  cshwrn  12422  limsupcl  12934  limsupgle  12938  limsuple  12939  limsupval2  12941  limsupgre  12942  isercolllem2  13126  isercoll  13128  isercoll2  13129  climsup  13130  ruclem11  13504  prmreclem6  13964  4sqlem11  13998  vdwapf  14015  vdwlem11  14034  0ram  14063  0ram2  14064  0ramcl  14066  imasdsval2  14436  mrcssv  14534  isacs1i  14577  funcres2b  14789  funcres2c  14793  setcepi  14938  yoniso  15077  isacs4lem  15320  acsmapd  15330  acsmap2d  15331  mhmima  15472  gsumval1  15488  gsumwspan  15503  frmdss2  15520  cycsubgcl  15686  cycsubgss  15687  ghmrn  15739  conjnmz  15759  cntzmhm  15835  f1omvdconj  15931  psgnunilem1  15978  dfod2  16044  odcl2  16045  odf1o2  16051  sylow1lem2  16077  pgpssslw  16092  sylow2blem1  16098  lsmssv  16121  lsmidm  16140  pj1ghm2  16180  efgsp1  16213  efgsfo  16215  efgrelexlemb  16226  cntzcmnf  16306  gexex  16314  iscyggen2  16337  cyggenod  16340  iscyg3  16342  gsumval3eu  16360  gsumval3OLD  16361  gsumval3lem1  16362  gsumval3lem2  16363  gsumval3  16364  gsumzsubmcl  16381  gsumzsubmclOLD  16382  gsumzaddlem  16387  gsumzadd  16388  gsumzaddlemOLD  16389  gsumzaddOLD  16390  gsumzsplit  16397  gsumzsplitOLD  16398  gsumconst  16405  gsumzoppg  16415  gsumzoppgOLD  16416  gsumpt  16428  gsumptOLD  16429  dmdprdd  16454  dprdfcntz  16472  dprdfcntzOLD  16478  dprdfeq0  16485  dprdfeq0OLD  16492  dprdlub  16496  dprdres  16498  dprdss  16499  dprdz  16500  dprdf1  16503  subgdmdprd  16504  subgdprd  16505  dprd2dlem1  16513  dprd2da  16514  dmdprdsplit2lem  16517  dpjghm2  16536  ablfac1b  16544  lmhmlsp  17051  pj1lmhm2  17103  aspval2  17338  mplbas2  17482  mplbas2OLD  17483  mplind  17515  pjfo  17981  frlmsplit2  18038  frlmsslsp  18064  frlmsslspOLD  18065  frlmlbs  18066  frlmup3  18069  frlmup4  18070  lindff1  18090  lindfrn  18091  f1lindf  18092  lindfmm  18097  indlcim  18110  iinopn  18356  tgiun  18425  pptbas  18453  tgrest  18604  resttopon  18606  rest0  18614  restfpw  18624  ordtbaslem  18633  ordtuni  18635  ordtbas2  18636  ordtrest  18647  ordtrest2  18649  leordtval2  18657  lecldbas  18664  cnclsi  18717  cnrest  18730  cnrest2r  18732  cnprest2  18735  lmss  18743  cncmp  18836  rncmp  18840  discmp  18842  cmpsub  18844  tgcmp  18845  hauscmplem  18850  bwthOLD  18855  conima  18870  concn  18871  2ndcctbss  18900  2ndcdisj  18901  2ndcomap  18903  2ndcsep  18904  dis2ndc  18905  lly1stc  18941  kgentop  18956  kgencmp  18959  1stckgenlem  18967  1stckgen  18968  kgencn2  18971  kgencn3  18972  txuni2  18979  ptbasfi  18995  xkoopn  19003  xkouni  19013  txbasval  19020  xkoccn  19033  ptcnplem  19035  upxp  19037  uptx  19039  txtube  19054  txcmplem1  19055  txcmplem2  19056  tx1stc  19064  txkgen  19066  xkoptsub  19068  xkoco1cn  19071  xkoco2cn  19072  xkococnlem  19073  xkococn  19074  xkoinjcn  19101  hmeores  19185  hmphdis  19210  fbasrn  19298  trfilss  19303  trfg  19305  zfbas  19310  uzrest  19311  elfm  19361  imaelfm  19365  rnelfmlem  19366  fclscmpi  19443  alexsublem  19457  alexsubALT  19464  ptcmplem1  19465  ptcmplem3  19467  cnextcn  19480  tmdgsum2  19508  symgtgp  19513  submtmd  19516  subgtgp  19517  subgntr  19518  opnsubg  19519  clsnsg  19521  tgpconcomp  19524  tsmsfbas  19539  tsmsxplem1  19568  prdsdsf  19783  prdsxmetlem  19784  prdsmet  19786  imasdsf1olem  19789  unirnblps  19835  unirnbl  19836  blin2  19845  imasf1oxms  19905  prdsbl  19907  met1stc  19937  met2ndci  19938  prdsxmslem2  19945  tgqioo  20218  xrtgioo  20224  xrge0gsumle  20251  xrge0tsms  20252  metdcn2  20257  metdsf  20265  metdsge  20266  metdscn2  20274  cnmptre  20340  iimulcn  20351  icchmeo  20354  xrhmeo  20359  cnheiborlem  20367  bndth  20371  evth  20372  evth2  20373  lebnumlem2  20375  lebnumlem3  20376  reparphti  20410  tchex  20573  tchnmfval  20584  fmcfil  20624  causs  20650  bcthlem5  20680  minveclem1  20752  minveclem3b  20756  evthicc2  20785  ovolficcss  20794  elovolm  20799  ovolmge0  20801  ovollb  20803  ovolgelb  20804  ovollb2lem  20812  ovollb2  20813  ovolunlem1a  20820  ovolunlem1  20821  ovoliunlem1  20826  ovoliunlem2  20827  ovoliun  20829  ovoliun2  20830  ovolscalem1  20837  ovolicc1  20840  ovolicc2lem4  20844  ovolicc2  20846  voliunlem2  20873  voliunlem3  20874  volsup  20878  ioombl1lem2  20881  ioombl1lem4  20883  uniioovol  20900  uniiccvol  20901  uniioombllem1  20902  uniioombllem2  20904  uniioombllem3  20906  uniioombllem6  20909  uniioombl  20910  dyadmbllem  20920  dyadmbl  20921  opnmbllem  20922  opnmblALT  20924  volsup2  20926  vitalilem2  20930  vitalilem4  20932  vitalilem5  20933  mbfconstlem  20948  mbfsup  20983  mbfinf  20984  mbflimsup  20985  i1fima  20997  i1fima2  20998  i1fd  21000  itg1cl  21004  itg1ge0  21005  i1f1  21009  itg11  21010  i1fmullem  21013  i1fadd  21014  i1fmul  21015  itg1addlem4  21018  itg1addlem5  21019  i1fmulc  21022  itg1mulc  21023  i1fres  21024  itg10a  21029  itg1ge0a  21030  itg1climres  21033  mbfi1fseqlem4  21037  itg2seq  21061  itg2monolem1  21069  itg2monolem2  21070  itg2monolem3  21071  itg2mono  21072  itg2i1fseq2  21075  itg2gt0  21079  itg2cnlem1  21080  itg2cn  21082  limciun  21210  c1liplem1  21309  dvne0  21324  dvne0f1  21325  lhop2  21328  dvcnvrelem2  21331  dvcnvre  21332  evlslem1  21366  evlseu  21367  mdegleb  21419  mdeglt  21420  mdegldg  21421  mdegxrcl  21422  mdegcl  21424  ig1peu  21527  aalioulem3  21684  ulmss  21746  reeff1o  21796  efifo  21887  dvlog  21980  efopn  21987  logccv  21992  efrlim  22247  basellem3  22304  fsumvma  22436  lgseisenlem4  22575  dchrisum0fno1  22644  ghsubgolem  23679  ubthlem1  24093  minvecolem1  24097  htthlem  24141  hhssims  24498  shsss  24538  pjrni  24927  imaelshi  25284  ofrn  25780  ofrn2  25781  xppreima2  25788  xrge0tsmsd  26105  ordtrestNEW  26204  ordtrest2NEW  26206  xrge0mulc1cn  26224  rge0scvg  26232  esumcst  26367  esumpfinvallem  26376  esumpcvgval  26380  esumcvg  26388  sibfinima  26572  sitgclg  26575  sitgclbn  26576  eulerpartgbij  26602  eulerpartlemgvv  26606  eulerpartlemgf  26609  rrvrnss  26677  orvcval4  26690  ballotlemsima  26745  lgamcvg2  26888  erdsze2lem2  26939  cvxpcon  26978  cvxscon  26979  cvmsss2  27010  cvmliftlem8  27028  cvmlift3lem6  27060  ghomgrpilem2  27151  ghomfo  27156  orderseqlem  27559  norn  27638  heicant  28267  opnmbllem0  28268  mblfinlem1  28269  mblfinlem2  28270  mblfinlem3  28271  mblfinlem4  28272  ismblfin  28273  volsupnfl  28277  itg2addnclem2  28285  itg2gt0cn  28288  ftc1anclem3  28310  ftc1anclem5  28312  ftc1anclem6  28313  ftc1anclem7  28314  ftc1anclem8  28315  ftc1anc  28316  comppfsc  28420  neibastop2lem  28422  tailfb  28439  indexdom  28469  cnresima  28504  istotbnd3  28511  sstotbnd2  28514  sstotbnd  28515  totbndbnd  28529  prdsbnd  28533  cntotbnd  28536  ismtyima  28543  heibor1lem  28549  heiborlem1  28551  heibor  28561  rrnval  28567  rrnequiv  28575  reheibor  28579  elrfirn  28873  cmpfiiin  28875  isnacs2  28884  isnacs3  28888  nacsfix  28890  coeq0i  28933  diophrw  28939  eldioph2lem2  28941  dnwech  29243  fnwe2lem2  29246  lmhmfgima  29279  pwssplit4  29284  hbt  29328  refsumcn  29594  cncmpmax  29596  climinf  29622  fafvelrn  29919  f0rn0  29984  frgrancvvdeqlem8  30476  lsatset  32205  lsatlss  32211  cdleme50rnlem  33758
  Copyright terms: Public domain W3C validator