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

Theorem frn 5556
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 5417 . 2  |-  ( F : A --> B  <->  ( F  Fn  A  /\  ran  F  C_  B ) )
21simprbi 451 1  |-  ( F : A --> B  ->  ran  F  C_  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    C_ wss 3280   ran crn 4838    Fn wfn 5408   -->wf 5409
This theorem is referenced by:  fco2  5560  fssxp  5561  fimacnvdisj  5580  f00  5587  foconst  5623  fun11iun  5654  fimacnv  5821  ffvelrn  5827  f1ompt  5850  fnfvrnss  5855  rnmptss  5856  f1dmex  5930  fliftrel  5989  isofr2  6023  fo1stres  6329  fo2ndres  6330  1stcof  6333  2ndcof  6334  fo2ndf  6412  fnwelem  6420  tposf2  6462  iunon  6559  iinon  6561  onoviun  6564  onnseq  6565  smores2  6575  seqomlem2  6667  oacomf1olem  6766  map0b  7011  mapsn  7014  f1imaen2g  7127  domdifsn  7150  domunsncan  7167  omxpenlem  7168  fodomr  7217  domss2  7225  f1finf1o  7294  f1fi  7352  unirnffid  7356  fissuni  7369  fipreima  7370  indexfi  7372  intrnfi  7379  dffi3  7394  ordtypelem8  7450  ordtypelem9  7451  ordtypelem10  7452  oismo  7465  hartogslem1  7467  brwdom2  7497  unxpwdom2  7512  ixpiunwdom  7515  infdifsn  7567  cantnf  7605  ac10ct  7871  numacn  7886  acndom  7888  acndom2  7891  infpwfien  7899  carduniima  7933  dfac12lem2  7980  dfac12lem3  7981  ackbij1  8074  fictb  8081  cfflb  8095  fin23lem40  8187  fin23lem41  8188  isf34lem5  8214  isf34lem7  8215  isf34lem6  8216  enfin1ai  8220  fin1a2lem6  8241  fin1a2lem7  8242  hsmexlem4  8265  hsmexlem5  8266  axdc2lem  8284  axdc3lem2  8287  ttukeylem6  8350  unirnfdomd  8398  pwcfsdom  8414  smobeth  8417  canthp1lem2  8484  pwfseqlem5  8494  wuncval2  8578  tskurn  8620  wfgru  8647  peano5nni  9959  rpnnen1lem4  10559  rpnnen1lem5  10560  unirnioo  10960  fseqsupcl  11271  fseqsupubi  11272  hashf1lem1  11659  hashf1lem2  11660  limsupcl  12222  limsupgle  12226  limsuple  12227  limsupval2  12229  limsupgre  12230  isercolllem2  12414  isercoll  12416  isercoll2  12417  climsup  12418  ruclem11  12794  prmreclem6  13244  4sqlem11  13278  vdwapf  13295  vdwlem11  13314  0ram  13343  0ram2  13344  0ramcl  13346  imasdsval2  13697  mrcssv  13794  isacs1i  13837  funcres2b  14049  funcres2c  14053  setcepi  14198  yoniso  14337  isacs4lem  14549  acsmapd  14559  acsmap2d  14560  mhmima  14718  gsumval1  14734  gsumwspan  14746  frmdss2  14763  cycsubgcl  14921  cycsubgss  14922  ghmrn  14974  conjnmz  14994  cntzmhm  15092  dfod2  15155  odcl2  15156  odf1o2  15162  sylow1lem2  15188  pgpssslw  15203  sylow2blem1  15209  lsmssv  15232  lsmidm  15251  pj1ghm2  15291  efgsp1  15324  efgsfo  15326  efgrelexlemb  15337  gexex  15423  iscyggen2  15446  cyggenod  15449  iscyg3  15451  gsumval3eu  15468  gsumval3  15469  cntzcmnf  15470  gsumzsubmcl  15478  gsumzaddlem  15481  gsumzadd  15482  gsumzsplit  15484  gsumconst  15487  gsumzoppg  15494  gsumpt  15500  dmdprdd  15515  dprdfcntz  15528  dprdfeq0  15535  dprdlub  15539  dprdres  15541  dprdss  15542  dprdz  15543  dprdf1  15546  subgdmdprd  15547  subgdprd  15548  dprd2dlem1  15554  dprd2da  15555  dmdprdsplit2lem  15558  dpjghm2  15577  ablfac1b  15583  lmhmlsp  16080  pj1lmhm2  16128  aspval2  16360  mplbas2  16486  mplind  16517  pjfo  16897  iinopn  16930  tgiun  16999  pptbas  17027  tgrest  17177  resttopon  17179  rest0  17187  restfpw  17197  ordtbaslem  17206  ordtuni  17208  ordtbas2  17209  ordtrest  17220  ordtrest2  17222  leordtval2  17230  lecldbas  17237  cnclsi  17290  cnrest  17303  cnrest2r  17305  cnprest2  17308  lmss  17316  cncmp  17409  rncmp  17413  discmp  17415  cmpsub  17417  tgcmp  17418  hauscmplem  17423  conima  17441  concn  17442  2ndcctbss  17471  2ndcdisj  17472  2ndcomap  17474  2ndcsep  17475  dis2ndc  17476  lly1stc  17512  kgentop  17527  kgencmp  17530  1stckgenlem  17538  1stckgen  17539  kgencn2  17542  kgencn3  17543  txuni2  17550  ptbasfi  17566  xkoopn  17574  xkouni  17584  txbasval  17591  xkoccn  17604  ptcnplem  17606  upxp  17608  uptx  17610  txtube  17625  txcmplem1  17626  txcmplem2  17627  tx1stc  17635  txkgen  17637  xkoptsub  17639  xkoco1cn  17642  xkoco2cn  17643  xkococnlem  17644  xkococn  17645  xkoinjcn  17672  hmeores  17756  hmphdis  17781  fbasrn  17869  trfilss  17874  trfg  17876  zfbas  17881  uzrest  17882  elfm  17932  imaelfm  17936  rnelfmlem  17937  fclscmpi  18014  alexsublem  18028  alexsubALT  18035  ptcmplem1  18036  ptcmplem3  18038  cnextcn  18051  tmdgsum2  18079  symgtgp  18084  submtmd  18087  subgtgp  18088  subgntr  18089  opnsubg  18090  clsnsg  18092  tgpconcomp  18095  tsmsfbas  18110  tsmsxplem1  18135  prdsdsf  18350  prdsxmetlem  18351  prdsmet  18353  imasdsf1olem  18356  unirnblps  18402  unirnbl  18403  blin2  18412  imasf1oxms  18472  prdsbl  18474  met1stc  18504  met2ndci  18505  prdsxmslem2  18512  tgqioo  18784  xrtgioo  18790  xrge0gsumle  18817  xrge0tsms  18818  metdcn2  18823  metdsf  18831  metdsge  18832  metdscn2  18840  cnmptre  18905  iimulcn  18916  icchmeo  18919  xrhmeo  18924  cnheiborlem  18932  bndth  18936  evth  18937  evth2  18938  lebnumlem2  18940  lebnumlem3  18941  reparphti  18975  tchex  19129  tchnmfval  19139  fmcfil  19178  causs  19204  bcthlem5  19234  minveclem1  19278  minveclem3b  19282  evthicc2  19310  ovolficcss  19319  elovolm  19324  ovolmge0  19326  ovollb  19328  ovolgelb  19329  ovollb2lem  19337  ovollb2  19338  ovolunlem1a  19345  ovolunlem1  19346  ovoliunlem1  19351  ovoliunlem2  19352  ovoliun  19354  ovoliun2  19355  ovolscalem1  19362  ovolicc1  19365  ovolicc2lem4  19369  ovolicc2  19371  voliunlem2  19398  voliunlem3  19399  volsup  19403  ioombl1lem2  19406  ioombl1lem4  19408  uniioovol  19424  uniiccvol  19425  uniioombllem1  19426  uniioombllem2  19428  uniioombllem3  19430  uniioombllem6  19433  uniioombl  19434  dyadmbllem  19444  dyadmbl  19445  opnmbllem  19446  opnmblALT  19448  volsup2  19450  vitalilem2  19454  vitalilem4  19456  vitalilem5  19457  mbfconstlem  19474  mbfsup  19509  mbfinf  19510  mbflimsup  19511  i1fima  19523  i1fima2  19524  i1fd  19526  itg1cl  19530  itg1ge0  19531  i1f1  19535  itg11  19536  i1fmullem  19539  i1fadd  19540  i1fmul  19541  itg1addlem4  19544  itg1addlem5  19545  i1fmulc  19548  itg1mulc  19549  i1fres  19550  itg10a  19555  itg1ge0a  19556  itg1climres  19559  mbfi1fseqlem4  19563  itg2seq  19587  itg2monolem1  19595  itg2monolem2  19596  itg2monolem3  19597  itg2mono  19598  itg2i1fseq2  19601  itg2gt0  19605  itg2cnlem1  19606  itg2cn  19608  limciun  19734  c1liplem1  19833  dvne0  19848  dvne0f1  19849  lhop2  19852  dvcnvrelem2  19855  dvcnvre  19856  evlslem1  19889  evlseu  19890  mdegleb  19940  mdeglt  19941  mdegldg  19942  mdegxrcl  19943  mdegcl  19945  ig1peu  20047  aalioulem3  20204  ulmss  20266  reeff1o  20316  efifo  20402  dvlog  20495  efopn  20502  logccv  20507  efrlim  20761  basellem3  20818  fsumvma  20950  lgseisenlem4  21089  dchrisum0fno1  21158  ghsubgolem  21911  ubthlem1  22325  minvecolem1  22329  htthlem  22373  hhssims  22728  shsss  22768  pjrni  23157  imaelshi  23514  ofrn  24005  ofrn2  24006  xppreima2  24013  xrge0tsmsd  24176  xrge0mulc1cn  24280  rge0scvg  24288  esumcst  24408  esumpfinvallem  24417  esumpcvgval  24421  esumcvg  24429  sitgclg  24609  sitgclbn  24610  rrvrnss  24658  orvcval4  24671  ballotlemsima  24726  lgamcvg2  24792  erdsze2lem2  24843  cvxpcon  24882  cvxscon  24883  cvmsss2  24914  cvmliftlem8  24932  cvmlift3lem6  24964  ghomgrpilem2  25050  ghomfo  25055  orderseqlem  25466  norn  25519  mblfinlem  26143  mblfinlem2  26144  mblfinlem3  26145  ismblfin  26146  volsupnfl  26150  itg2addnclem2  26156  itg2gt0cn  26159  comppfsc  26277  neibastop2lem  26279  tailfb  26296  indexdom  26326  cnresima  26363  istotbnd3  26370  sstotbnd2  26373  sstotbnd  26374  totbndbnd  26388  prdsbnd  26392  cntotbnd  26395  ismtyima  26402  heibor1lem  26408  heiborlem1  26410  heibor  26420  rrnval  26426  rrnequiv  26434  reheibor  26438  elrfirn  26639  cmpfiiin  26641  isnacs2  26650  isnacs3  26654  nacsfix  26656  coeq0i  26701  diophrw  26707  eldioph2lem2  26709  dnwech  27013  fnwe2lem2  27016  lmhmfgima  27050  pwssplit4  27059  frlmsplit2  27111  frlmsslsp  27116  frlmlbs  27117  frlmup3  27120  frlmup4  27121  lindff1  27158  lindfrn  27159  f1lindf  27160  lindfmm  27165  indlcim  27178  hbt  27202  f1omvdconj  27257  psgnunilem1  27284  refsumcn  27568  cncmpmax  27570  climinf  27599  fafvelrn  27901  hashimarn  27994  frgrancvvdeqlem8  28143  lsatset  29473  lsatlss  29479  cdleme50rnlem  31026
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 178  df-an 361  df-f 5417
  Copyright terms: Public domain W3C validator