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

Theorem frn 5530
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 5391 . 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 3256   ran crn 4812    Fn wfn 5382   -->wf 5383
This theorem is referenced by:  fco2  5534  fssxp  5535  fimacnvdisj  5554  f00  5561  foconst  5597  fun11iun  5628  fimacnv  5794  ffvelrn  5800  f1ompt  5823  fnfvrnss  5828  rnmptss  5829  f1dmex  5903  fliftrel  5962  isofr2  5996  fo1stres  6302  fo2ndres  6303  1stcof  6306  2ndcof  6307  fnwelem  6390  tposf2  6432  iunon  6529  iinon  6531  onoviun  6534  onnseq  6535  smores2  6545  seqomlem2  6637  oacomf1olem  6736  map0b  6981  mapsn  6984  f1imaen2g  7097  domdifsn  7120  domunsncan  7137  omxpenlem  7138  fodomr  7187  domss2  7195  f1finf1o  7264  f1fi  7322  unirnffid  7326  fissuni  7339  fipreima  7340  indexfi  7342  intrnfi  7349  dffi3  7364  ordtypelem8  7420  ordtypelem9  7421  ordtypelem10  7422  oismo  7435  hartogslem1  7437  brwdom2  7467  unxpwdom2  7482  ixpiunwdom  7485  infdifsn  7537  cantnf  7575  ac10ct  7841  numacn  7856  acndom  7858  acndom2  7861  infpwfien  7869  carduniima  7903  dfac12lem2  7950  dfac12lem3  7951  ackbij1  8044  fictb  8051  cfflb  8065  fin23lem40  8157  fin23lem41  8158  isf34lem5  8184  isf34lem7  8185  isf34lem6  8186  enfin1ai  8190  fin1a2lem6  8211  fin1a2lem7  8212  hsmexlem4  8235  hsmexlem5  8236  axdc2lem  8254  axdc3lem2  8257  ttukeylem6  8320  unirnfdomd  8368  pwcfsdom  8384  smobeth  8387  canthp1lem2  8454  pwfseqlem5  8464  wuncval2  8548  tskurn  8590  wfgru  8617  peano5nni  9928  rpnnen1lem4  10528  rpnnen1lem5  10529  unirnioo  10929  fseqsupcl  11236  fseqsupubi  11237  hashf1rn  11556  hashf1lem1  11624  hashf1lem2  11625  limsupcl  12187  limsupgle  12191  limsuple  12192  limsupval2  12194  limsupgre  12195  isercolllem2  12379  isercoll  12381  isercoll2  12382  climsup  12383  ruclem11  12759  prmreclem6  13209  4sqlem11  13243  vdwapf  13260  vdwlem11  13279  0ram  13308  0ram2  13309  0ramcl  13311  imasdsval2  13662  mrcssv  13759  isacs1i  13802  funcres2b  14014  funcres2c  14018  setcepi  14163  yoniso  14302  isacs4lem  14514  acsmapd  14524  acsmap2d  14525  mhmima  14683  gsumval1  14699  gsumwspan  14711  frmdss2  14728  cycsubgcl  14886  cycsubgss  14887  ghmrn  14939  conjnmz  14959  cntzmhm  15057  dfod2  15120  odcl2  15121  odf1o2  15127  sylow1lem2  15153  pgpssslw  15168  sylow2blem1  15174  lsmssv  15197  lsmidm  15216  pj1ghm2  15256  efgsp1  15289  efgsfo  15291  efgrelexlemb  15302  gexex  15388  iscyggen2  15411  cyggenod  15414  iscyg3  15416  gsumval3eu  15433  gsumval3  15434  cntzcmnf  15435  gsumzsubmcl  15443  gsumzaddlem  15446  gsumzadd  15447  gsumzsplit  15449  gsumconst  15452  gsumzoppg  15459  gsumpt  15465  dmdprdd  15480  dprdfcntz  15493  dprdfeq0  15500  dprdlub  15504  dprdres  15506  dprdss  15507  dprdz  15508  dprdf1  15511  subgdmdprd  15512  subgdprd  15513  dprd2dlem1  15519  dprd2da  15520  dmdprdsplit2lem  15523  dpjghm2  15542  ablfac1b  15548  lmhmlsp  16045  pj1lmhm2  16093  aspval2  16325  mplbas2  16451  mplind  16482  pjfo  16858  iinopn  16891  tgiun  16960  pptbas  16988  tgrest  17138  resttopon  17140  rest0  17148  restfpw  17158  ordtbaslem  17167  ordtuni  17169  ordtbas2  17170  ordtrest  17181  ordtrest2  17183  leordtval2  17191  lecldbas  17198  cnclsi  17251  cnrest  17264  cnrest2r  17266  cnprest2  17269  lmss  17277  cncmp  17370  rncmp  17374  discmp  17376  cmpsub  17378  tgcmp  17379  hauscmplem  17384  conima  17402  concn  17403  2ndcctbss  17432  2ndcdisj  17433  2ndcomap  17435  2ndcsep  17436  dis2ndc  17437  lly1stc  17473  kgentop  17488  kgencmp  17491  1stckgenlem  17499  1stckgen  17500  kgencn2  17503  kgencn3  17504  txuni2  17511  ptbasfi  17527  xkoopn  17535  xkouni  17545  txbasval  17552  xkoccn  17565  ptcnplem  17567  upxp  17569  uptx  17571  txtube  17586  txcmplem1  17587  txcmplem2  17588  tx1stc  17596  txkgen  17598  xkoptsub  17600  xkoco1cn  17603  xkoco2cn  17604  xkococnlem  17605  xkococn  17606  xkoinjcn  17633  hmeores  17717  hmphdis  17742  fbasrn  17830  trfilss  17835  trfg  17837  zfbas  17842  uzrest  17843  elfm  17893  imaelfm  17897  rnelfmlem  17898  fclscmpi  17975  alexsublem  17989  alexsubALT  17996  ptcmplem1  17997  ptcmplem3  17999  cnextcn  18012  tmdgsum2  18040  symgtgp  18045  submtmd  18048  subgtgp  18049  subgntr  18050  opnsubg  18051  clsnsg  18053  tgpconcomp  18056  tsmsfbas  18071  tsmsxplem1  18096  prdsdsf  18298  prdsxmetlem  18299  prdsmet  18301  imasdsf1olem  18304  unirnbl  18336  blin2  18342  imasf1oxms  18402  prdsbl  18404  met1stc  18434  met2ndci  18435  prdsxmslem2  18442  tgqioo  18695  xrtgioo  18701  xrge0gsumle  18728  xrge0tsms  18729  metdcn2  18734  metdsf  18742  metdsge  18743  metdscn2  18751  cnmptre  18816  iimulcn  18827  icchmeo  18830  xrhmeo  18835  cnheiborlem  18843  bndth  18847  evth  18848  evth2  18849  lebnumlem2  18851  lebnumlem3  18852  reparphti  18886  tchex  19040  tchnmfval  19050  fmcfil  19089  causs  19115  bcthlem5  19143  minveclem1  19185  minveclem3b  19189  evthicc2  19217  ovolficcss  19226  elovolm  19231  ovolmge0  19233  ovollb  19235  ovolgelb  19236  ovollb2lem  19244  ovollb2  19245  ovolunlem1a  19252  ovolunlem1  19253  ovoliunlem1  19258  ovoliunlem2  19259  ovoliun  19261  ovoliun2  19262  ovolscalem1  19269  ovolicc1  19272  ovolicc2lem4  19276  ovolicc2  19278  voliunlem2  19305  voliunlem3  19306  volsup  19310  ioombl1lem2  19313  ioombl1lem4  19315  uniioovol  19331  uniiccvol  19332  uniioombllem1  19333  uniioombllem2  19335  uniioombllem3  19337  uniioombllem6  19340  uniioombl  19341  dyadmbllem  19351  dyadmbl  19352  opnmbllem  19353  opnmblALT  19355  volsup2  19357  vitalilem2  19361  vitalilem4  19363  vitalilem5  19364  mbfconstlem  19381  mbfsup  19416  mbfinf  19417  mbflimsup  19418  i1fima  19430  i1fima2  19431  i1fd  19433  itg1cl  19437  itg1ge0  19438  i1f1  19442  itg11  19443  i1fmullem  19446  i1fadd  19447  i1fmul  19448  itg1addlem4  19451  itg1addlem5  19452  i1fmulc  19455  itg1mulc  19456  i1fres  19457  itg10a  19462  itg1ge0a  19463  itg1climres  19466  mbfi1fseqlem4  19470  itg2seq  19494  itg2monolem1  19502  itg2monolem2  19503  itg2monolem3  19504  itg2mono  19505  itg2i1fseq2  19508  itg2gt0  19512  itg2cnlem1  19513  itg2cn  19515  limciun  19641  c1liplem1  19740  dvne0  19755  dvne0f1  19756  lhop2  19759  dvcnvrelem2  19762  dvcnvre  19763  evlslem1  19796  evlseu  19797  mdegleb  19847  mdeglt  19848  mdegldg  19849  mdegxrcl  19850  mdegcl  19852  ig1peu  19954  aalioulem3  20111  ulmss  20173  reeff1o  20223  efifo  20309  dvlog  20402  efopn  20409  logccv  20414  efrlim  20668  basellem3  20725  fsumvma  20857  lgseisenlem4  20996  dchrisum0fno1  21065  ghsubgolem  21799  ubthlem1  22213  minvecolem1  22217  htthlem  22261  hhssims  22616  shsss  22656  pjrni  23045  imaelshi  23402  ofrn  23888  ofrn2  23889  xppreima2  23895  xrge0tsmsd  24045  xrge0mulc1cn  24124  rge0scvg  24132  esumcst  24244  esumpfinvallem  24253  esumpcvgval  24257  esumcvg  24265  rrvrnss  24477  orvcval4  24490  ballotlemsima  24545  lgamcvg2  24611  erdsze2lem2  24662  cvxpcon  24701  cvxscon  24702  cvmsss2  24733  cvmliftlem8  24751  cvmlift3lem6  24783  ghomgrpilem2  24869  ghomfo  24874  orderseqlem  25269  norn  25322  volsupnfl  25949  itg2addnclem2  25951  itg2gt0cn  25953  comppfsc  26071  neibastop2lem  26073  tailfb  26090  indexdom  26120  cnresima  26157  istotbnd3  26164  sstotbnd2  26167  sstotbnd  26168  totbndbnd  26182  prdsbnd  26186  cntotbnd  26189  ismtyima  26196  heibor1lem  26202  heiborlem1  26204  heibor  26214  rrnval  26220  rrnequiv  26228  reheibor  26232  elrfirn  26433  cmpfiiin  26435  isnacs2  26444  isnacs3  26448  nacsfix  26450  coeq0i  26495  diophrw  26501  eldioph2lem2  26503  dnwech  26807  fnwe2lem2  26810  lmhmfgima  26844  pwssplit4  26853  frlmsplit2  26905  frlmsslsp  26910  frlmlbs  26911  frlmup3  26914  frlmup4  26915  lindff1  26952  lindfrn  26953  f1lindf  26954  lindfmm  26959  indlcim  26972  hbt  26996  f1omvdconj  27051  psgnunilem1  27078  refsumcn  27362  cncmpmax  27364  climinf  27393  fafvelrn  27696  frgrancvvdeqlem8  27785  lsatset  29156  lsatlss  29162  cdleme50rnlem  30709
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 5391
  Copyright terms: Public domain W3C validator