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

Theorem frn 5663
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 5520 . 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 3426   ran crn 4939    Fn wfn 5511   -->wf 5512
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 5520
This theorem is referenced by:  fco2  5667  fssxp  5668  fimacnvdisj  5687  f00  5691  foconst  5729  fimacnv  5934  ffvelrn  5940  f1ompt  5964  fnfvrnss  5970  rnmptss  5971  fliftrel  6100  isofr2  6134  fun11iun  6637  f1dmex  6647  fo1stres  6700  fo2ndres  6701  1stcof  6704  2ndcof  6705  fo2ndf  6779  fnwelem  6787  tposf2  6869  iunon  6899  iinon  6901  onoviun  6904  onnseq  6905  smores2  6915  seqomlem2  7006  oacomf1olem  7103  map0b  7351  mapsn  7354  f1imaen2g  7470  domdifsn  7494  domunsncan  7511  omxpenlem  7512  fodomr  7562  domss2  7570  f1finf1o  7640  f1fi  7699  unirnffid  7704  fissuni  7717  fipreima  7718  indexfi  7720  intrnfi  7767  dffi3  7782  ordtypelem8  7840  ordtypelem9  7841  ordtypelem10  7842  oismo  7855  hartogslem1  7857  brwdom2  7889  unxpwdom2  7904  ixpiunwdom  7907  infdifsn  7963  cantnf  8002  cantnfOLD  8024  ac10ct  8305  numacn  8320  acndom  8322  acndom2  8325  infpwfien  8333  carduniima  8367  dfac12lem2  8414  dfac12lem3  8415  ackbij1  8508  fictb  8515  cfflb  8529  fin23lem40  8621  fin23lem41  8622  isf34lem5  8648  isf34lem7  8649  isf34lem6  8650  enfin1ai  8654  fin1a2lem6  8675  fin1a2lem7  8676  hsmexlem4  8699  hsmexlem5  8700  axdc2lem  8718  axdc3lem2  8721  ttukeylem6  8784  unirnfdomd  8832  pwcfsdom  8848  smobeth  8851  canthp1lem2  8921  pwfseqlem5  8931  wuncval2  9015  tskurn  9057  wfgru  9084  peano5nni  10426  rpnnen1lem4  11083  rpnnen1lem5  11084  unirnioo  11490  fseqsupcl  11900  fseqsupubi  11901  hashimarn  12302  hashf1lem1  12310  hashf1lem2  12311  swrdrn  12425  cshwrn  12541  limsupcl  13053  limsupgle  13057  limsuple  13058  limsupval2  13060  limsupgre  13061  isercolllem2  13245  isercoll  13247  isercoll2  13248  climsup  13249  ruclem11  13624  prmreclem6  14084  4sqlem11  14118  vdwapf  14135  vdwlem11  14154  0ram  14183  0ram2  14184  0ramcl  14186  imasdsval2  14556  mrcssv  14654  isacs1i  14697  funcres2b  14909  funcres2c  14913  setcepi  15058  yoniso  15197  isacs4lem  15440  acsmapd  15450  acsmap2d  15451  mhmima  15593  gsumval1  15611  gsumwspan  15626  frmdss2  15643  cycsubgcl  15809  cycsubgss  15810  ghmrn  15862  conjnmz  15882  cntzmhm  15958  f1omvdconj  16054  psgnunilem1  16101  dfod2  16169  odcl2  16170  odf1o2  16176  sylow1lem2  16202  pgpssslw  16217  sylow2blem1  16223  lsmssv  16246  lsmidm  16265  pj1ghm2  16305  efgsp1  16338  efgsfo  16340  efgrelexlemb  16351  cntzcmnf  16431  gexex  16439  iscyggen2  16462  cyggenod  16465  iscyg3  16467  gsumval3eu  16485  gsumval3OLD  16486  gsumval3lem1  16487  gsumval3lem2  16488  gsumval3  16489  gsumzsubmcl  16506  gsumzsubmclOLD  16507  gsumzaddlem  16512  gsumzadd  16513  gsumzaddlemOLD  16514  gsumzaddOLD  16515  gsumzsplit  16522  gsumzsplitOLD  16523  gsumconst  16532  gsumzoppg  16545  gsumzoppgOLD  16546  gsumpt  16559  gsumptOLD  16560  dmdprdd  16586  dprdfcntz  16604  dprdfcntzOLD  16610  dprdfeq0  16617  dprdfeq0OLD  16624  dprdlub  16628  dprdres  16630  dprdss  16631  dprdz  16632  dprdf1  16635  subgdmdprd  16636  subgdprd  16637  dprd2dlem1  16645  dprd2da  16646  dmdprdsplit2lem  16649  dpjghm2  16668  ablfac1b  16676  lmhmlsp  17236  pj1lmhm2  17288  aspval2  17523  mplcoe5lem  17654  mplbas2  17658  mplbas2OLD  17659  mplind  17691  evlslem1  17708  evlseu  17709  gsumply1subr  17795  pjfo  18249  frlmsplit2  18306  frlmsslsp  18332  frlmsslspOLD  18333  frlmlbs  18334  frlmup3  18337  frlmup4  18338  lindff1  18358  lindfrn  18359  f1lindf  18360  lindfmm  18365  indlcim  18378  iinopn  18631  tgiun  18700  pptbas  18728  tgrest  18879  resttopon  18881  rest0  18889  restfpw  18899  ordtbaslem  18908  ordtuni  18910  ordtbas2  18911  ordtrest  18922  ordtrest2  18924  leordtval2  18932  lecldbas  18939  cnclsi  18992  cnrest  19005  cnrest2r  19007  cnprest2  19010  lmss  19018  cncmp  19111  rncmp  19115  discmp  19117  cmpsub  19119  tgcmp  19120  hauscmplem  19125  bwthOLD  19130  conima  19145  concn  19146  2ndcctbss  19175  2ndcdisj  19176  2ndcomap  19178  2ndcsep  19179  dis2ndc  19180  lly1stc  19216  kgentop  19231  kgencmp  19234  1stckgenlem  19242  1stckgen  19243  kgencn2  19246  kgencn3  19247  txuni2  19254  ptbasfi  19270  xkoopn  19278  xkouni  19288  txbasval  19295  xkoccn  19308  ptcnplem  19310  upxp  19312  uptx  19314  txtube  19329  txcmplem1  19330  txcmplem2  19331  tx1stc  19339  txkgen  19341  xkoptsub  19343  xkoco1cn  19346  xkoco2cn  19347  xkococnlem  19348  xkococn  19349  xkoinjcn  19376  hmeores  19460  hmphdis  19485  fbasrn  19573  trfilss  19578  trfg  19580  zfbas  19585  uzrest  19586  elfm  19636  imaelfm  19640  rnelfmlem  19641  fclscmpi  19718  alexsublem  19732  alexsubALT  19739  ptcmplem1  19740  ptcmplem3  19742  cnextcn  19755  tmdgsum2  19783  symgtgp  19788  submtmd  19791  subgtgp  19792  subgntr  19793  opnsubg  19794  clsnsg  19796  tgpconcomp  19799  tsmsfbas  19814  tsmsxplem1  19843  prdsdsf  20058  prdsxmetlem  20059  prdsmet  20061  imasdsf1olem  20064  unirnblps  20110  unirnbl  20111  blin2  20120  imasf1oxms  20180  prdsbl  20182  met1stc  20212  met2ndci  20213  prdsxmslem2  20220  tgqioo  20493  xrtgioo  20499  xrge0gsumle  20526  xrge0tsms  20527  metdcn2  20532  metdsf  20540  metdsge  20541  metdscn2  20549  cnmptre  20615  iimulcn  20626  icchmeo  20629  xrhmeo  20634  cnheiborlem  20642  bndth  20646  evth  20647  evth2  20648  lebnumlem2  20650  lebnumlem3  20651  reparphti  20685  tchex  20848  tchnmfval  20859  fmcfil  20899  causs  20925  bcthlem5  20955  minveclem1  21027  minveclem3b  21031  evthicc2  21060  ovolficcss  21069  elovolm  21074  ovolmge0  21076  ovollb  21078  ovolgelb  21079  ovollb2lem  21087  ovollb2  21088  ovolunlem1a  21095  ovolunlem1  21096  ovoliunlem1  21101  ovoliunlem2  21102  ovoliun  21104  ovoliun2  21105  ovolscalem1  21112  ovolicc1  21115  ovolicc2lem4  21119  ovolicc2  21121  voliunlem2  21148  voliunlem3  21149  volsup  21153  ioombl1lem2  21156  ioombl1lem4  21158  uniioovol  21175  uniiccvol  21176  uniioombllem1  21177  uniioombllem2  21179  uniioombllem3  21181  uniioombllem6  21184  uniioombl  21185  dyadmbllem  21195  dyadmbl  21196  opnmbllem  21197  opnmblALT  21199  volsup2  21201  vitalilem2  21205  vitalilem4  21207  vitalilem5  21208  mbfconstlem  21223  mbfsup  21258  mbfinf  21259  mbflimsup  21260  i1fima  21272  i1fima2  21273  i1fd  21275  itg1cl  21279  itg1ge0  21280  i1f1  21284  itg11  21285  i1fmullem  21288  i1fadd  21289  i1fmul  21290  itg1addlem4  21293  itg1addlem5  21294  i1fmulc  21297  itg1mulc  21298  i1fres  21299  itg10a  21304  itg1ge0a  21305  itg1climres  21308  mbfi1fseqlem4  21312  itg2seq  21336  itg2monolem1  21344  itg2monolem2  21345  itg2monolem3  21346  itg2mono  21347  itg2i1fseq2  21350  itg2gt0  21354  itg2cnlem1  21355  itg2cn  21357  limciun  21485  c1liplem1  21584  dvne0  21599  dvne0f1  21600  lhop2  21603  dvcnvrelem2  21606  dvcnvre  21607  mdegleb  21651  mdeglt  21652  mdegldg  21653  mdegxrcl  21654  mdegcl  21656  ig1peu  21759  aalioulem3  21916  ulmss  21978  reeff1o  22028  efifo  22119  dvlog  22212  efopn  22219  logccv  22224  efrlim  22479  basellem3  22536  fsumvma  22668  lgseisenlem4  22807  dchrisum0fno1  22876  ghsubgolem  23992  ubthlem1  24406  minvecolem1  24410  htthlem  24454  hhssims  24811  shsss  24851  pjrni  25240  imaelshi  25597  ofrn  26091  ofrn2  26092  xppreima2  26099  xrge0tsmsd  26387  ordtrestNEW  26485  ordtrest2NEW  26487  xrge0mulc1cn  26505  rge0scvg  26513  esumcst  26648  esumpfinvallem  26657  esumpcvgval  26661  esumcvg  26669  sibfinima  26859  sitgclg  26862  sitgclbn  26863  eulerpartgbij  26889  eulerpartlemgvv  26893  eulerpartlemgf  26896  rrvrnss  26964  orvcval4  26977  ballotlemsima  27032  lgamcvg2  27175  erdsze2lem2  27226  cvxpcon  27265  cvxscon  27266  cvmsss2  27297  cvmliftlem8  27315  cvmlift3lem6  27347  ghomgrpilem2  27439  ghomfo  27444  orderseqlem  27847  norn  27926  heicant  28564  opnmbllem0  28565  mblfinlem1  28566  mblfinlem2  28567  mblfinlem3  28568  mblfinlem4  28569  ismblfin  28570  volsupnfl  28574  itg2addnclem2  28582  itg2gt0cn  28585  ftc1anclem3  28607  ftc1anclem5  28609  ftc1anclem6  28610  ftc1anclem7  28611  ftc1anclem8  28612  ftc1anc  28613  comppfsc  28717  neibastop2lem  28719  tailfb  28736  indexdom  28766  cnresima  28801  istotbnd3  28808  sstotbnd2  28811  sstotbnd  28812  totbndbnd  28826  prdsbnd  28830  cntotbnd  28833  ismtyima  28840  heibor1lem  28846  heiborlem1  28848  heibor  28858  rrnval  28864  rrnequiv  28872  reheibor  28876  elrfirn  29169  cmpfiiin  29171  isnacs2  29180  isnacs3  29184  nacsfix  29186  coeq0i  29229  diophrw  29235  eldioph2lem2  29237  dnwech  29539  fnwe2lem2  29542  lmhmfgima  29575  pwssplit4  29580  hbt  29624  refsumcn  29890  cncmpmax  29892  climinf  29917  fafvelrn  30214  f0rn0  30279  frgrancvvdeqlem8  30771  m2cpmf1  31206  m2cpmghm  31207  m2cpmmhm  31208  lsatset  32941  lsatlss  32947  cdleme50rnlem  34494
  Copyright terms: Public domain W3C validator