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

Theorem frn 5727
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 5582 . 2  |-  ( F : A --> B  <->  ( F  Fn  A  /\  ran  F  C_  B ) )
21simprbi 464 1  |-  ( F : A --> B  ->  ran  F  C_  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    C_ wss 3461   ran crn 4990    Fn wfn 5573   -->wf 5574
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 5582
This theorem is referenced by:  fco2  5732  fssxp  5733  fimacnvdisj  5753  f00  5757  f0rn0  5760  foconst  5796  fimacnv  6004  ffvelrn  6014  f1ompt  6038  fnfvrnss  6044  rnmptss  6045  fliftrel  6191  isofr2  6225  fun11iun  6745  f1dmex  6755  fo1stres  6809  fo2ndres  6810  1stcof  6813  2ndcof  6814  fo2ndf  6892  fnwelem  6900  tposf2  6981  onoviun  7016  onnseq  7017  smores2  7027  seqomlem2  7118  oacomf1olem  7215  map0b  7459  mapsn  7462  f1imaen2g  7578  domdifsn  7602  domunsncan  7619  omxpenlem  7620  fodomr  7670  domss2  7678  f1finf1o  7748  f1fi  7809  unirnffid  7814  fissuni  7827  fipreima  7828  indexfi  7830  intrnfi  7878  dffi3  7893  ordtypelem8  7953  ordtypelem9  7954  ordtypelem10  7955  oismo  7968  hartogslem1  7970  brwdom2  8002  unxpwdom2  8017  ixpiunwdom  8020  infdifsn  8076  cantnf  8115  cantnfOLD  8137  ac10ct  8418  numacn  8433  acndom  8435  acndom2  8438  infpwfien  8446  carduniima  8480  dfac12lem2  8527  dfac12lem3  8528  ackbij1  8621  fictb  8628  cfflb  8642  fin23lem40  8734  fin23lem41  8735  isf34lem5  8761  isf34lem7  8762  isf34lem6  8763  enfin1ai  8767  fin1a2lem6  8788  fin1a2lem7  8789  hsmexlem4  8812  hsmexlem5  8813  axdc2lem  8831  axdc3lem2  8834  ttukeylem6  8897  unirnfdomd  8945  pwcfsdom  8961  smobeth  8964  canthp1lem2  9034  pwfseqlem5  9044  wuncval2  9128  tskurn  9170  wfgru  9197  peano5nni  10546  rpnnen1lem4  11222  rpnnen1lem5  11223  unirnioo  11635  fseqsupcl  12069  fseqsupubi  12070  hashimarn  12478  hashf1lem1  12486  hashf1lem2  12487  ccatrn  12588  swrdrn  12636  cshwrn  12755  limsupcl  13278  limsupgle  13282  limsuple  13283  limsupval2  13285  limsupgre  13286  isercolllem2  13470  isercoll  13472  isercoll2  13473  climsup  13474  ruclem11  13955  prmreclem6  14421  4sqlem11  14455  vdwapf  14472  vdwlem11  14491  0ram  14520  0ram2  14521  0ramcl  14523  imasdsval2  14895  mrcssv  14993  isacs1i  15036  funcres2b  15245  funcres2c  15249  setcepi  15394  yoniso  15533  isacs4lem  15777  acsmapd  15787  acsmap2d  15788  gsumval1  15883  mhmima  15973  gsumwspan  15993  frmdss2  16010  cycsubgcl  16206  cycsubgss  16207  ghmrn  16259  conjnmz  16279  cntzmhm  16355  f1omvdconj  16450  psgnunilem1  16497  dfod2  16565  odcl2  16566  odf1o2  16572  sylow1lem2  16598  pgpssslw  16613  sylow2blem1  16619  lsmssv  16642  lsmidm  16661  pj1ghm2  16701  efgsp1  16734  efgsfo  16736  efgrelexlemb  16747  cntzcmnf  16830  gexex  16838  iscyggen2  16863  cyggenod  16866  iscyg3  16868  gsumval3eu  16886  gsumval3OLD  16887  gsumval3lem1  16888  gsumval3lem2  16889  gsumval3  16890  gsumzsubmcl  16907  gsumzsubmclOLD  16908  gsumzaddlem  16913  gsumzadd  16914  gsumzaddlemOLD  16915  gsumzaddOLD  16916  gsumzsplit  16923  gsumzsplitOLD  16924  gsumconst  16933  gsumzoppg  16946  gsumzoppgOLD  16947  gsumpt  16967  gsumptOLD  16968  dmdprdd  17009  dprdfcntz  17028  dprdfcntzOLD  17034  dprdfeq0  17041  dprdfeq0OLD  17048  dprdlub  17052  dprdres  17054  dprdss  17055  dprdz  17056  dprdf1  17059  subgdmdprd  17060  subgdprd  17061  dprd2dlem1  17069  dprd2da  17070  dmdprdsplit2lem  17073  dpjghm2  17092  ablfac1b  17100  lmhmlsp  17674  pj1lmhm2  17726  aspval2  17975  mplcoe5lem  18109  mplbas2  18113  mplbas2OLD  18114  mplind  18146  evlslem1  18163  evlseu  18164  gsumply1subr  18254  pjfo  18724  frlmsplit2  18781  frlmsslsp  18807  frlmsslspOLD  18808  frlmlbs  18809  frlmup3  18812  frlmup4  18813  lindff1  18833  lindfrn  18834  f1lindf  18835  lindfmm  18840  indlcim  18853  m2cpmf1  19222  m2cpmghm  19223  m2cpmmhm  19224  iinopn  19389  pptbas  19487  tgrest  19638  resttopon  19640  rest0  19648  restfpw  19658  ordtbaslem  19667  ordtuni  19669  ordtbas2  19670  ordtrest  19681  ordtrest2  19683  leordtval2  19691  lecldbas  19698  cnclsi  19751  cnrest2r  19766  cnprest2  19769  lmss  19777  cncmp  19870  rncmp  19874  discmp  19876  cmpsub  19878  tgcmp  19879  hauscmplem  19884  bwthOLD  19889  conima  19904  concn  19905  2ndcctbss  19934  2ndcdisj  19935  2ndcomap  19937  2ndcsep  19938  dis2ndc  19939  lly1stc  19975  comppfsc  20011  kgentop  20021  kgencmp  20024  1stckgenlem  20032  1stckgen  20033  kgencn2  20036  kgencn3  20037  txuni2  20044  ptbasfi  20060  xkoopn  20068  xkouni  20078  txbasval  20085  xkoccn  20098  ptcnplem  20100  upxp  20102  uptx  20104  txtube  20119  txcmplem1  20120  txcmplem2  20121  tx1stc  20129  txkgen  20131  xkoptsub  20133  xkoco1cn  20136  xkoco2cn  20137  xkococnlem  20138  xkococn  20139  xkoinjcn  20166  hmeores  20250  hmphdis  20275  fbasrn  20363  trfilss  20368  trfg  20370  zfbas  20375  uzrest  20376  elfm  20426  imaelfm  20430  rnelfmlem  20431  fclscmpi  20508  alexsublem  20522  alexsubALT  20529  ptcmplem1  20530  ptcmplem3  20532  cnextcn  20545  tmdgsum2  20573  symgtgp  20578  submtmd  20581  subgtgp  20582  subgntr  20583  opnsubg  20584  clsnsg  20586  tgpconcomp  20589  tsmsfbas  20604  tsmsxplem1  20633  prdsdsf  20848  prdsxmetlem  20849  prdsmet  20851  imasdsf1olem  20854  unirnblps  20900  unirnbl  20901  blin2  20910  imasf1oxms  20970  prdsbl  20972  met1stc  21002  met2ndci  21003  prdsxmslem2  21010  tgqioo  21283  xrtgioo  21289  xrge0gsumle  21316  xrge0tsms  21317  metdcn2  21322  metdsf  21330  metdsge  21331  metdscn2  21339  cnmptre  21405  iimulcn  21416  icchmeo  21419  xrhmeo  21424  cnheiborlem  21432  bndth  21436  evth  21437  evth2  21438  lebnumlem2  21440  lebnumlem3  21441  reparphti  21475  tchex  21638  tchnmfval  21649  fmcfil  21689  causs  21715  bcthlem5  21745  minveclem1  21817  minveclem3b  21821  evthicc2  21850  ovolficcss  21859  elovolm  21864  ovolmge0  21866  ovollb  21868  ovolgelb  21869  ovollb2lem  21877  ovollb2  21878  ovolunlem1a  21885  ovolunlem1  21886  ovoliunlem1  21891  ovoliunlem2  21892  ovoliun  21894  ovoliun2  21895  ovolscalem1  21902  ovolicc1  21905  ovolicc2lem4  21909  ovolicc2  21911  voliunlem2  21939  voliunlem3  21940  volsup  21944  ioombl1lem2  21947  ioombl1lem4  21949  uniioovol  21966  uniiccvol  21967  uniioombllem1  21968  uniioombllem2  21970  uniioombllem3  21972  uniioombllem6  21975  uniioombl  21976  dyadmbllem  21986  dyadmbl  21987  opnmbllem  21988  opnmblALT  21990  volsup2  21992  vitalilem2  21996  vitalilem4  21998  vitalilem5  21999  mbfconstlem  22014  mbfsup  22049  mbfinf  22050  mbflimsup  22051  i1fima  22063  i1fima2  22064  i1fd  22066  itg1cl  22070  itg1ge0  22071  i1f1  22075  itg11  22076  i1fmullem  22079  i1fadd  22080  i1fmul  22081  itg1addlem4  22084  itg1addlem5  22085  i1fmulc  22088  itg1mulc  22089  i1fres  22090  itg10a  22095  itg1ge0a  22096  itg1climres  22099  mbfi1fseqlem4  22103  itg2seq  22127  itg2monolem1  22135  itg2monolem2  22136  itg2monolem3  22137  itg2mono  22138  itg2i1fseq2  22141  itg2gt0  22145  itg2cnlem1  22146  itg2cn  22148  limciun  22276  c1liplem1  22375  dvne0  22390  dvne0f1  22391  lhop2  22394  dvcnvrelem2  22397  dvcnvre  22398  mdegleb  22442  mdeglt  22443  mdegldg  22444  mdegxrcl  22445  mdegcl  22447  ig1peu  22550  aalioulem3  22708  ulmss  22770  reeff1o  22820  efifo  22912  dvlog  23010  efopn  23017  logccv  23022  efrlim  23277  basellem3  23334  fsumvma  23466  lgseisenlem4  23605  dchrisum0fno1  23674  edgss  24330  frgrancvvdeqlem8  25018  ghsubgolemOLD  25350  ubthlem1  25764  minvecolem1  25768  htthlem  25812  hhssims  26169  shsss  26209  pjrni  26598  imaelshi  26955  foresf1o  27381  ofrn  27457  ofrn2  27458  fimarab  27461  xppreima2  27466  xrge0tsmsd  27753  locfinreflem  27821  cmpcref  27831  ordtrestNEW  27881  ordtrest2NEW  27883  xrge0mulc1cn  27901  rge0scvg  27909  esumcst  28049  esumpfinvallem  28058  esumpcvgval  28062  esumcvg  28070  sibfinima  28259  sitgclg  28262  sitgclbn  28263  eulerpartgbij  28289  eulerpartlemgvv  28293  eulerpartlemgf  28296  rrvrnss  28364  orvcval4  28377  ballotlemsima  28432  lgamcvg2  28575  erdsze2lem2  28626  cvxpcon  28665  cvxscon  28666  cvmsss2  28697  cvmliftlem8  28715  cvmlift3lem6  28747  mrsubrn  28851  mrsubf  28855  msubrn  28867  msubf  28870  mstapst  28885  mvtss  28891  mclsssvlem  28900  mclsax  28907  mclsind  28908  mclsppslem  28921  ghomgrpilem2  29004  ghomfo  29009  orderseqlem  29308  norn  29387  heicant  30025  opnmbllem0  30026  mblfinlem1  30027  mblfinlem2  30028  mblfinlem3  30029  mblfinlem4  30030  ismblfin  30031  volsupnfl  30035  itg2addnclem2  30043  itg2gt0cn  30046  ftc1anclem3  30068  ftc1anclem5  30070  ftc1anclem6  30071  ftc1anclem7  30072  ftc1anclem8  30073  ftc1anc  30074  neibastop2lem  30154  tailfb  30171  indexdom  30201  cnresima  30236  istotbnd3  30243  sstotbnd2  30246  sstotbnd  30247  totbndbnd  30261  prdsbnd  30265  cntotbnd  30268  ismtyima  30275  heibor1lem  30281  heiborlem1  30283  heibor  30293  rrnval  30299  rrnequiv  30307  reheibor  30311  elrfirn  30603  cmpfiiin  30605  isnacs2  30614  isnacs3  30618  nacsfix  30620  coeq0i  30662  diophrw  30668  eldioph2lem2  30670  dnwech  30970  fnwe2lem2  30973  lmhmfgima  31006  pwssplit4  31011  hbt  31055  refsumcn  31359  cncmpmax  31361  climinf  31566  icccncfext  31644  dvsinax  31662  itgsubsticclem  31728  fourierdlem12  31855  fourierdlem42  31885  fourierdlem54  31897  fourierdlem70  31913  fourierdlem76  31919  fourierdlem82  31925  fourierdlem85  31928  fourierdlem88  31931  fourierdlem93  31936  fourierdlem113  31956  fafvelrn  32209  mgmplusfreseq  32415  mgmhmima  32444  lsatset  34590  lsatlss  34596  cdleme50rnlem  36145  imo72b2lem0  37786  imo72b2lem2  37788  imo72b2lem1  37792  imo72b2  37797
  Copyright terms: Public domain W3C validator