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

Theorem frn 5475
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 5338 . 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 3228   ran crn 4769    Fn wfn 5329   -->wf 5330
This theorem is referenced by:  fco2  5479  fssxp  5480  fimacnvdisj  5499  f00  5506  foconst  5542  fun11iun  5573  fimacnv  5737  ffvelrn  5743  f1ompt  5762  fnfvrnss  5767  f1dmex  5834  fliftrel  5891  isofr2  5925  fo1stres  6227  fo2ndres  6228  1stcof  6231  2ndcof  6232  fnwelem  6314  tposf2  6342  iunon  6439  iinon  6441  onoviun  6444  onnseq  6445  smores2  6455  seqomlem2  6547  oacomf1olem  6646  map0b  6891  mapsn  6894  f1imaen2g  7007  domdifsn  7030  domunsncan  7047  omxpenlem  7048  fodomr  7097  domss2  7105  f1finf1o  7173  f1fi  7230  unirnffid  7234  fissuni  7247  fipreima  7248  indexfi  7250  intrnfi  7257  dffi3  7271  ordtypelem8  7327  ordtypelem9  7328  ordtypelem10  7329  oismo  7342  hartogslem1  7344  brwdom2  7374  unxpwdom2  7389  ixpiunwdom  7392  infdifsn  7444  cantnf  7482  ac10ct  7748  numacn  7763  acndom  7765  acndom2  7768  infpwfien  7776  carduniima  7810  dfac12lem2  7857  dfac12lem3  7858  ackbij1  7951  fictb  7958  cfflb  7972  fin23lem40  8064  fin23lem41  8065  isf34lem5  8091  isf34lem7  8092  isf34lem6  8093  enfin1ai  8097  fin1a2lem6  8118  fin1a2lem7  8119  hsmexlem4  8142  hsmexlem5  8143  axdc2lem  8161  axdc3lem2  8164  ttukeylem6  8228  unirnfdomd  8276  pwcfsdom  8292  smobeth  8295  canthp1lem2  8362  pwfseqlem5  8372  wuncval2  8456  tskurn  8498  wfgru  8525  peano5nni  9836  rpnnen1lem4  10434  rpnnen1lem5  10435  unirnioo  10832  fseqsupcl  11128  fseqsupubi  11129  hashf1lem1  11483  hashf1lem2  11484  limsupcl  12037  limsupgle  12041  limsuple  12042  limsupval2  12044  limsupgre  12045  isercolllem2  12229  isercoll  12231  isercoll2  12232  climsup  12233  ruclem11  12609  prmreclem6  13059  4sqlem11  13093  vdwapf  13110  vdwlem11  13129  0ram  13158  0ram2  13159  0ramcl  13161  imasdsval2  13512  mrcssv  13609  isacs1i  13652  funcres2b  13864  funcres2c  13868  setcepi  14013  yoniso  14152  isacs4lem  14364  acsmapd  14374  acsmap2d  14375  mhmima  14533  gsumval1  14549  gsumwspan  14561  frmdss2  14578  cycsubgcl  14736  cycsubgss  14737  ghmrn  14789  conjnmz  14809  cntzmhm  14907  dfod2  14970  odcl2  14971  odf1o2  14977  sylow1lem2  15003  pgpssslw  15018  sylow2blem1  15024  lsmssv  15047  lsmidm  15066  pj1ghm2  15106  efgsp1  15139  efgsfo  15141  efgrelexlemb  15152  gexex  15238  iscyggen2  15261  cyggenod  15264  iscyg3  15266  gsumval3eu  15283  gsumval3  15284  cntzcmnf  15285  gsumzsubmcl  15293  gsumzaddlem  15296  gsumzadd  15297  gsumzsplit  15299  gsumconst  15302  gsumzoppg  15309  gsumpt  15315  dmdprdd  15330  dprdfcntz  15343  dprdfeq0  15350  dprdlub  15354  dprdres  15356  dprdss  15357  dprdz  15358  dprdf1  15361  subgdmdprd  15362  subgdprd  15363  dprd2dlem1  15369  dprd2da  15370  dmdprdsplit2lem  15373  dpjghm2  15392  ablfac1b  15398  lmhmlsp  15899  pj1lmhm2  15947  aspval2  16179  mplbas2  16305  mplind  16336  pjfo  16715  iinopn  16748  tgiun  16817  pptbas  16845  tgrest  16990  resttopon  16992  rest0  17000  restfpw  17010  ordtbaslem  17018  ordtuni  17020  ordtbas2  17021  ordtrest  17032  ordtrest2  17034  leordtval2  17042  lecldbas  17049  cnclsi  17101  cnrest  17113  cnrest2r  17115  cnprest2  17118  lmss  17126  cncmp  17219  rncmp  17223  discmp  17225  cmpsub  17227  tgcmp  17228  hauscmplem  17233  conima  17251  concn  17252  2ndcctbss  17281  2ndcdisj  17282  2ndcomap  17284  2ndcsep  17285  dis2ndc  17286  lly1stc  17322  kgentop  17337  kgencmp  17340  1stckgenlem  17348  1stckgen  17349  kgencn2  17352  kgencn3  17353  txuni2  17360  ptbasfi  17376  xkoopn  17384  xkouni  17394  txbasval  17401  xkoccn  17413  ptcnplem  17415  upxp  17417  uptx  17419  txtube  17434  txcmplem1  17435  txcmplem2  17436  tx1stc  17444  txkgen  17446  xkoptsub  17448  xkoco1cn  17451  xkoco2cn  17452  xkococnlem  17453  xkococn  17454  xkoinjcn  17481  hmeores  17562  hmphdis  17587  fbasrn  17675  trfilss  17680  trfg  17682  zfbas  17687  uzrest  17688  elfm  17738  imaelfm  17742  rnelfmlem  17743  fclscmpi  17820  alexsublem  17834  alexsubALT  17841  ptcmplem1  17842  ptcmplem3  17844  tmdgsum2  17875  symgtgp  17880  submtmd  17883  subgtgp  17884  subgntr  17885  opnsubg  17886  clsnsg  17888  tgpconcomp  17891  tsmsfbas  17906  tsmsxplem1  17931  prdsdsf  18027  prdsxmetlem  18028  prdsmet  18030  imasdsf1olem  18033  unirnbl  18065  blin2  18071  imasf1oxms  18131  prdsbl  18133  met1stc  18163  met2ndci  18164  prdsxmslem2  18171  tgqioo  18402  xrtgioo  18408  xrge0gsumle  18435  xrge0tsms  18436  metdcn2  18441  metdsf  18449  metdsge  18450  metdscn2  18458  cnmptre  18523  iimulcn  18534  icchmeo  18537  xrhmeo  18542  cnheiborlem  18550  bndth  18554  evth  18555  evth2  18556  lebnumlem2  18558  lebnumlem3  18559  reparphti  18593  tchex  18747  tchnmfval  18757  fmcfil  18796  causs  18822  bcthlem5  18848  minveclem1  18886  minveclem3b  18890  evthicc2  18918  ovolficcss  18927  elovolm  18932  ovolmge0  18934  ovollb  18936  ovolgelb  18937  ovollb2lem  18945  ovollb2  18946  ovolunlem1a  18953  ovolunlem1  18954  ovoliunlem1  18959  ovoliunlem2  18960  ovoliun  18962  ovoliun2  18963  ovolscalem1  18970  ovolicc1  18973  ovolicc2lem4  18977  ovolicc2  18979  voliunlem2  19006  voliunlem3  19007  volsup  19011  ioombl1lem2  19014  ioombl1lem4  19016  uniioovol  19032  uniiccvol  19033  uniioombllem1  19034  uniioombllem2  19036  uniioombllem3  19038  uniioombllem6  19041  uniioombl  19042  dyadmbllem  19052  dyadmbl  19053  opnmbllem  19054  opnmblALT  19056  volsup2  19058  vitalilem2  19062  vitalilem4  19064  vitalilem5  19065  mbfconstlem  19082  mbfsup  19117  mbfinf  19118  mbflimsup  19119  i1fima  19131  i1fima2  19132  i1fd  19134  itg1cl  19138  itg1ge0  19139  i1f1  19143  itg11  19144  i1fmullem  19147  i1fadd  19148  i1fmul  19149  itg1addlem4  19152  itg1addlem5  19153  i1fmulc  19156  itg1mulc  19157  i1fres  19158  itg10a  19163  itg1ge0a  19164  itg1climres  19167  mbfi1fseqlem4  19171  itg2seq  19195  itg2monolem1  19203  itg2monolem2  19204  itg2monolem3  19205  itg2mono  19206  itg2i1fseq2  19209  itg2gt0  19213  itg2cnlem1  19214  itg2cn  19216  limciun  19342  c1liplem1  19441  dvne0  19456  dvne0f1  19457  lhop2  19460  dvcnvrelem2  19463  dvcnvre  19464  evlslem1  19497  evlseu  19498  mdegleb  19548  mdeglt  19549  mdegldg  19550  mdegxrcl  19551  mdegcl  19553  ig1peu  19655  aalioulem3  19812  ulmss  19874  reeff1o  19924  efifo  20010  dvlog  20103  efopn  20110  logccv  20115  efrlim  20369  basellem3  20426  fsumvma  20558  lgseisenlem4  20697  dchrisum0fno1  20766  ghsubgolem  21143  ubthlem1  21557  minvecolem1  21561  htthlem  21605  hhssims  21960  shsss  22000  pjrni  22389  imaelshi  22746  ofrn  23253  ofrn2  23254  xppreima2  23260  rnmptss  23286  xrge0tsmsd  23415  xrge0mulc1cn  23483  rge0scvg  23491  cnextcn  23504  esumcst  23721  esumpfinvallem  23730  esumpcvgval  23734  esumcvg  23742  rrvrnss  23954  orvcval4  23967  ballotlemsima  24022  lgamcvg2  24088  erdsze2lem2  24139  cvxpcon  24177  cvxscon  24178  cvmsss2  24209  cvmliftlem8  24227  cvmlift3lem6  24259  ghomgrpilem2  24397  ghomfo  24402  orderseqlem  24810  norn  24863  volsupnfl  25491  itg2addnclem2  25493  itg2gt0cn  25495  comppfsc  25631  neibastop2lem  25633  tailfb  25650  indexdom  25737  cnresima  25807  istotbnd3  25818  sstotbnd2  25821  sstotbnd  25822  totbndbnd  25836  prdsbnd  25840  cntotbnd  25843  ismtyima  25850  heibor1lem  25856  heiborlem1  25858  heibor  25868  rrnval  25874  rrnequiv  25882  reheibor  25886  elrfirn  26093  cmpfiiin  26095  isnacs2  26104  isnacs3  26108  nacsfix  26110  coeq0i  26155  diophrw  26161  eldioph2lem2  26163  dnwech  26468  fnwe2lem2  26471  lmhmfgima  26505  pwssplit4  26514  frlmsplit2  26566  frlmsslsp  26571  frlmlbs  26572  frlmup3  26575  frlmup4  26576  lindff1  26613  lindfrn  26614  f1lindf  26615  lindfmm  26620  indlcim  26633  hbt  26657  f1omvdconj  26712  psgnunilem1  26739  fnvinran  27008  refsumcn  27024  cncmpmax  27026  climinf  27055  fafvelrn  27358  hashf1rn  27486  frgrancvvdeqlem8  27856  lsatset  29232  lsatlss  29238  cdleme50rnlem  30785
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 5338
  Copyright terms: Public domain W3C validator