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

Theorem frn 5589
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 5450 . 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 3312   ran crn 4871    Fn wfn 5441   -->wf 5442
This theorem is referenced by:  fco2  5593  fssxp  5594  fimacnvdisj  5613  f00  5620  foconst  5656  fun11iun  5687  fimacnv  5854  ffvelrn  5860  f1ompt  5883  fnfvrnss  5888  rnmptss  5889  f1dmex  5963  fliftrel  6022  isofr2  6056  fo1stres  6362  fo2ndres  6363  1stcof  6366  2ndcof  6367  fo2ndf  6445  fnwelem  6453  tposf2  6495  iunon  6592  iinon  6594  onoviun  6597  onnseq  6598  smores2  6608  seqomlem2  6700  oacomf1olem  6799  map0b  7044  mapsn  7047  f1imaen2g  7160  domdifsn  7183  domunsncan  7200  omxpenlem  7201  fodomr  7250  domss2  7258  f1finf1o  7327  f1fi  7385  unirnffid  7390  fissuni  7403  fipreima  7404  indexfi  7406  intrnfi  7413  dffi3  7428  ordtypelem8  7486  ordtypelem9  7487  ordtypelem10  7488  oismo  7501  hartogslem1  7503  brwdom2  7533  unxpwdom2  7548  ixpiunwdom  7551  infdifsn  7603  cantnf  7641  ac10ct  7907  numacn  7922  acndom  7924  acndom2  7927  infpwfien  7935  carduniima  7969  dfac12lem2  8016  dfac12lem3  8017  ackbij1  8110  fictb  8117  cfflb  8131  fin23lem40  8223  fin23lem41  8224  isf34lem5  8250  isf34lem7  8251  isf34lem6  8252  enfin1ai  8256  fin1a2lem6  8277  fin1a2lem7  8278  hsmexlem4  8301  hsmexlem5  8302  axdc2lem  8320  axdc3lem2  8323  ttukeylem6  8386  unirnfdomd  8434  pwcfsdom  8450  smobeth  8453  canthp1lem2  8520  pwfseqlem5  8530  wuncval2  8614  tskurn  8656  wfgru  8683  peano5nni  9995  rpnnen1lem4  10595  rpnnen1lem5  10596  unirnioo  10996  fseqsupcl  11308  fseqsupubi  11309  hashf1lem1  11696  hashf1lem2  11697  limsupcl  12259  limsupgle  12263  limsuple  12264  limsupval2  12266  limsupgre  12267  isercolllem2  12451  isercoll  12453  isercoll2  12454  climsup  12455  ruclem11  12831  prmreclem6  13281  4sqlem11  13315  vdwapf  13332  vdwlem11  13351  0ram  13380  0ram2  13381  0ramcl  13383  imasdsval2  13734  mrcssv  13831  isacs1i  13874  funcres2b  14086  funcres2c  14090  setcepi  14235  yoniso  14374  isacs4lem  14586  acsmapd  14596  acsmap2d  14597  mhmima  14755  gsumval1  14771  gsumwspan  14783  frmdss2  14800  cycsubgcl  14958  cycsubgss  14959  ghmrn  15011  conjnmz  15031  cntzmhm  15129  dfod2  15192  odcl2  15193  odf1o2  15199  sylow1lem2  15225  pgpssslw  15240  sylow2blem1  15246  lsmssv  15269  lsmidm  15288  pj1ghm2  15328  efgsp1  15361  efgsfo  15363  efgrelexlemb  15374  gexex  15460  iscyggen2  15483  cyggenod  15486  iscyg3  15488  gsumval3eu  15505  gsumval3  15506  cntzcmnf  15507  gsumzsubmcl  15515  gsumzaddlem  15518  gsumzadd  15519  gsumzsplit  15521  gsumconst  15524  gsumzoppg  15531  gsumpt  15537  dmdprdd  15552  dprdfcntz  15565  dprdfeq0  15572  dprdlub  15576  dprdres  15578  dprdss  15579  dprdz  15580  dprdf1  15583  subgdmdprd  15584  subgdprd  15585  dprd2dlem1  15591  dprd2da  15592  dmdprdsplit2lem  15595  dpjghm2  15614  ablfac1b  15620  lmhmlsp  16117  pj1lmhm2  16165  aspval2  16397  mplbas2  16523  mplind  16554  pjfo  16934  iinopn  16967  tgiun  17036  pptbas  17064  tgrest  17215  resttopon  17217  rest0  17225  restfpw  17235  ordtbaslem  17244  ordtuni  17246  ordtbas2  17247  ordtrest  17258  ordtrest2  17260  leordtval2  17268  lecldbas  17275  cnclsi  17328  cnrest  17341  cnrest2r  17343  cnprest2  17346  lmss  17354  cncmp  17447  rncmp  17451  discmp  17453  cmpsub  17455  tgcmp  17456  hauscmplem  17461  bwth  17465  conima  17480  concn  17481  2ndcctbss  17510  2ndcdisj  17511  2ndcomap  17513  2ndcsep  17514  dis2ndc  17515  lly1stc  17551  kgentop  17566  kgencmp  17569  1stckgenlem  17577  1stckgen  17578  kgencn2  17581  kgencn3  17582  txuni2  17589  ptbasfi  17605  xkoopn  17613  xkouni  17623  txbasval  17630  xkoccn  17643  ptcnplem  17645  upxp  17647  uptx  17649  txtube  17664  txcmplem1  17665  txcmplem2  17666  tx1stc  17674  txkgen  17676  xkoptsub  17678  xkoco1cn  17681  xkoco2cn  17682  xkococnlem  17683  xkococn  17684  xkoinjcn  17711  hmeores  17795  hmphdis  17820  fbasrn  17908  trfilss  17913  trfg  17915  zfbas  17920  uzrest  17921  elfm  17971  imaelfm  17975  rnelfmlem  17976  fclscmpi  18053  alexsublem  18067  alexsubALT  18074  ptcmplem1  18075  ptcmplem3  18077  cnextcn  18090  tmdgsum2  18118  symgtgp  18123  submtmd  18126  subgtgp  18127  subgntr  18128  opnsubg  18129  clsnsg  18131  tgpconcomp  18134  tsmsfbas  18149  tsmsxplem1  18174  prdsdsf  18389  prdsxmetlem  18390  prdsmet  18392  imasdsf1olem  18395  unirnblps  18441  unirnbl  18442  blin2  18451  imasf1oxms  18511  prdsbl  18513  met1stc  18543  met2ndci  18544  prdsxmslem2  18551  tgqioo  18823  xrtgioo  18829  xrge0gsumle  18856  xrge0tsms  18857  metdcn2  18862  metdsf  18870  metdsge  18871  metdscn2  18879  cnmptre  18944  iimulcn  18955  icchmeo  18958  xrhmeo  18963  cnheiborlem  18971  bndth  18975  evth  18976  evth2  18977  lebnumlem2  18979  lebnumlem3  18980  reparphti  19014  tchex  19168  tchnmfval  19178  fmcfil  19217  causs  19243  bcthlem5  19273  minveclem1  19317  minveclem3b  19321  evthicc2  19349  ovolficcss  19358  elovolm  19363  ovolmge0  19365  ovollb  19367  ovolgelb  19368  ovollb2lem  19376  ovollb2  19377  ovolunlem1a  19384  ovolunlem1  19385  ovoliunlem1  19390  ovoliunlem2  19391  ovoliun  19393  ovoliun2  19394  ovolscalem1  19401  ovolicc1  19404  ovolicc2lem4  19408  ovolicc2  19410  voliunlem2  19437  voliunlem3  19438  volsup  19442  ioombl1lem2  19445  ioombl1lem4  19447  uniioovol  19463  uniiccvol  19464  uniioombllem1  19465  uniioombllem2  19467  uniioombllem3  19469  uniioombllem6  19472  uniioombl  19473  dyadmbllem  19483  dyadmbl  19484  opnmbllem  19485  opnmblALT  19487  volsup2  19489  vitalilem2  19493  vitalilem4  19495  vitalilem5  19496  mbfconstlem  19513  mbfsup  19548  mbfinf  19549  mbflimsup  19550  i1fima  19562  i1fima2  19563  i1fd  19565  itg1cl  19569  itg1ge0  19570  i1f1  19574  itg11  19575  i1fmullem  19578  i1fadd  19579  i1fmul  19580  itg1addlem4  19583  itg1addlem5  19584  i1fmulc  19587  itg1mulc  19588  i1fres  19589  itg10a  19594  itg1ge0a  19595  itg1climres  19598  mbfi1fseqlem4  19602  itg2seq  19626  itg2monolem1  19634  itg2monolem2  19635  itg2monolem3  19636  itg2mono  19637  itg2i1fseq2  19640  itg2gt0  19644  itg2cnlem1  19645  itg2cn  19647  limciun  19773  c1liplem1  19872  dvne0  19887  dvne0f1  19888  lhop2  19891  dvcnvrelem2  19894  dvcnvre  19895  evlslem1  19928  evlseu  19929  mdegleb  19979  mdeglt  19980  mdegldg  19981  mdegxrcl  19982  mdegcl  19984  ig1peu  20086  aalioulem3  20243  ulmss  20305  reeff1o  20355  efifo  20441  dvlog  20534  efopn  20541  logccv  20546  efrlim  20800  basellem3  20857  fsumvma  20989  lgseisenlem4  21128  dchrisum0fno1  21197  ghsubgolem  21950  ubthlem1  22364  minvecolem1  22368  htthlem  22412  hhssims  22767  shsss  22807  pjrni  23196  imaelshi  23553  ofrn  24044  ofrn2  24045  xppreima2  24052  xrge0tsmsd  24215  xrge0mulc1cn  24319  rge0scvg  24327  esumcst  24447  esumpfinvallem  24456  esumpcvgval  24460  esumcvg  24468  sitgclg  24648  sitgclbn  24649  rrvrnss  24697  orvcval4  24710  ballotlemsima  24765  lgamcvg2  24831  erdsze2lem2  24882  cvxpcon  24921  cvxscon  24922  cvmsss2  24953  cvmliftlem8  24971  cvmlift3lem6  25003  ghomgrpilem2  25089  ghomfo  25094  orderseqlem  25519  norn  25598  mblfinlem  26234  mblfinlem2  26235  mblfinlem3  26236  ismblfin  26237  volsupnfl  26241  itg2addnclem2  26247  itg2gt0cn  26250  ftc1anclem3  26272  ftc1anclem5  26274  ftc1anclem6  26275  ftc1anclem7  26276  ftc1anclem8  26277  ftc1anc  26278  comppfsc  26378  neibastop2lem  26380  tailfb  26397  indexdom  26427  cnresima  26464  istotbnd3  26471  sstotbnd2  26474  sstotbnd  26475  totbndbnd  26489  prdsbnd  26493  cntotbnd  26496  ismtyima  26503  heibor1lem  26509  heiborlem1  26511  heibor  26521  rrnval  26527  rrnequiv  26535  reheibor  26539  elrfirn  26740  cmpfiiin  26742  isnacs2  26751  isnacs3  26755  nacsfix  26757  coeq0i  26802  diophrw  26808  eldioph2lem2  26810  dnwech  27114  fnwe2lem2  27117  lmhmfgima  27150  pwssplit4  27159  frlmsplit2  27211  frlmsslsp  27216  frlmlbs  27217  frlmup3  27220  frlmup4  27221  lindff1  27258  lindfrn  27259  f1lindf  27260  lindfmm  27265  indlcim  27278  hbt  27302  f1omvdconj  27357  psgnunilem1  27384  refsumcn  27668  cncmpmax  27670  climinf  27699  fafvelrn  28001  hashimarn  28141  frgrancvvdeqlem8  28366  lsatset  29725  lsatlss  29731  cdleme50rnlem  31278
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 5450
  Copyright terms: Public domain W3C validator