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

Theorem frn 5658
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 5513 . 2  |-  ( F : A --> B  <->  ( F  Fn  A  /\  ran  F  C_  B ) )
21simprbi 462 1  |-  ( F : A --> B  ->  ran  F  C_  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    C_ wss 3402   ran crn 4927    Fn wfn 5504   -->wf 5505
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 369  df-f 5513
This theorem is referenced by:  fco2  5663  fssxp  5664  fimacnvdisj  5684  f00  5688  f0rn0  5691  foconst  5727  fimacnv  5934  ffvelrn  5944  f1ompt  5968  fnfvrnss  5974  rnmptss  5975  fliftrel  6125  isofr2  6159  fun11iun  6677  f1dmex  6687  fo1stres  6741  fo2ndres  6742  1stcof  6745  2ndcof  6746  fo2ndf  6824  fnwelem  6832  tposf2  6915  onoviun  6950  onnseq  6951  smores2  6961  seqomlem2  7052  oacomf1olem  7149  map0b  7394  mapsn  7397  f1imaen2g  7513  domdifsn  7537  domunsncan  7554  omxpenlem  7555  fodomr  7605  domss2  7613  f1finf1o  7680  f1fi  7740  unirnffid  7745  fissuni  7758  fipreima  7759  indexfi  7761  intrnfi  7809  dffi3  7824  ordtypelem8  7883  ordtypelem9  7884  ordtypelem10  7885  oismo  7898  hartogslem1  7900  brwdom2  7932  unxpwdom2  7947  ixpiunwdom  7950  infdifsn  8005  cantnf  8043  cantnfOLD  8065  ac10ct  8346  numacn  8361  acndom  8363  acndom2  8366  infpwfien  8374  carduniima  8408  dfac12lem2  8455  dfac12lem3  8456  ackbij1  8549  fictb  8556  cfflb  8570  fin23lem40  8662  fin23lem41  8663  isf34lem5  8689  isf34lem7  8690  isf34lem6  8691  enfin1ai  8695  fin1a2lem6  8716  fin1a2lem7  8717  hsmexlem4  8740  hsmexlem5  8741  axdc2lem  8759  axdc3lem2  8762  ttukeylem6  8825  unirnfdomd  8873  pwcfsdom  8889  smobeth  8892  canthp1lem2  8960  pwfseqlem5  8970  wuncval2  9054  tskurn  9096  wfgru  9123  peano5nni  10473  rpnnen1lem4  11148  rpnnen1lem5  11149  unirnioo  11563  fseqsupcl  12009  fseqsupubi  12010  hashimarn  12419  hashf1lem1  12427  hashf1lem2  12428  ccatrn  12534  swrdrn  12584  cshwrn  12703  limsupcl  13317  limsupgle  13321  limsuple  13322  limsupval2  13324  limsupgre  13325  isercolllem2  13509  isercoll  13511  isercoll2  13512  climsup  13513  ruclem11  13994  prmreclem6  14460  4sqlem11  14494  vdwapf  14511  vdwlem11  14530  0ram  14559  0ram2  14560  0ramcl  14562  imasdsval2  14942  mrcssv  15040  isacs1i  15083  funcres2b  15322  funcres2c  15326  setcepi  15503  yoniso  15690  isacs4lem  15934  acsmapd  15944  acsmap2d  15945  gsumval1  16040  mhmima  16130  gsumwspan  16150  frmdss2  16167  cycsubgcl  16363  cycsubgss  16364  ghmrn  16416  conjnmz  16436  cntzmhm  16512  f1omvdconj  16607  psgnunilem1  16654  dfod2  16722  odcl2  16723  odf1o2  16729  sylow1lem2  16755  pgpssslw  16770  sylow2blem1  16776  lsmssv  16799  lsmidm  16818  pj1ghm2  16858  efgsp1  16891  efgsfo  16893  efgrelexlemb  16904  cntzcmnf  16987  gexex  16995  iscyggen2  17020  cyggenod  17023  iscyg3  17025  gsumval3eu  17043  gsumval3OLD  17044  gsumval3lem1  17045  gsumval3lem2  17046  gsumval3  17047  gsumzsubmcl  17064  gsumzsubmclOLD  17065  gsumzaddlem  17070  gsumzadd  17071  gsumzaddlemOLD  17072  gsumzaddOLD  17073  gsumzsplit  17080  gsumzsplitOLD  17081  gsumconst  17089  gsumzoppg  17102  gsumzoppgOLD  17103  gsumpt  17121  gsumptOLD  17122  dmdprdd  17162  dprdfcntz  17181  dprdfcntzOLD  17187  dprdfeq0  17194  dprdfeq0OLD  17201  dprdlub  17205  dprdres  17207  dprdss  17208  dprdz  17209  dprdf1  17212  subgdmdprd  17213  subgdprd  17214  dprd2dlem1  17222  dprd2da  17223  dmdprdsplit2lem  17226  dpjghm2  17245  ablfac1b  17253  lmhmlsp  17827  pj1lmhm2  17879  aspval2  18128  mplcoe5lem  18262  mplbas2  18266  mplbas2OLD  18267  mplind  18299  evlslem1  18316  evlseu  18317  gsumply1subr  18407  pjfo  18856  frlmsplit2  18911  frlmsslsp  18935  frlmlbs  18936  frlmup3  18939  frlmup4  18940  lindff1  18959  lindfrn  18960  f1lindf  18961  lindfmm  18966  indlcim  18979  m2cpmf1  19348  m2cpmghm  19349  m2cpmmhm  19350  iinopn  19515  pptbas  19613  tgrest  19765  resttopon  19767  rest0  19775  restfpw  19785  ordtbaslem  19794  ordtuni  19796  ordtbas2  19797  ordtrest  19808  ordtrest2  19810  leordtval2  19818  lecldbas  19825  cnclsi  19878  cnrest2r  19893  cnprest2  19896  lmss  19904  cncmp  19997  rncmp  20001  discmp  20003  cmpsub  20005  tgcmp  20006  hauscmplem  20011  conima  20030  concn  20031  2ndcctbss  20060  2ndcdisj  20061  2ndcomap  20063  2ndcsep  20064  dis2ndc  20065  lly1stc  20101  comppfsc  20137  kgentop  20147  kgencmp  20150  1stckgenlem  20158  1stckgen  20159  kgencn2  20162  kgencn3  20163  txuni2  20170  ptbasfi  20186  xkoopn  20194  xkouni  20204  txbasval  20211  xkoccn  20224  ptcnplem  20226  upxp  20228  uptx  20230  txtube  20245  txcmplem1  20246  txcmplem2  20247  tx1stc  20255  txkgen  20257  xkoptsub  20259  xkoco1cn  20262  xkoco2cn  20263  xkococnlem  20264  xkococn  20265  xkoinjcn  20292  hmeores  20376  hmphdis  20401  fbasrn  20489  trfilss  20494  trfg  20496  zfbas  20501  uzrest  20502  elfm  20552  imaelfm  20556  rnelfmlem  20557  fclscmpi  20634  alexsublem  20648  alexsubALT  20655  ptcmplem1  20656  ptcmplem3  20658  cnextcn  20671  tmdgsum2  20699  symgtgp  20704  submtmd  20707  subgtgp  20708  subgntr  20709  opnsubg  20710  clsnsg  20712  tgpconcomp  20715  tsmsfbas  20730  tsmsxplem1  20759  prdsdsf  20974  prdsxmetlem  20975  prdsmet  20977  imasdsf1olem  20980  unirnblps  21026  unirnbl  21027  blin2  21036  imasf1oxms  21096  prdsbl  21098  met1stc  21128  met2ndci  21129  prdsxmslem2  21136  tgqioo  21409  xrtgioo  21415  xrge0gsumle  21442  xrge0tsms  21443  metdcn2  21448  metdsf  21456  metdsge  21457  metdscn2  21465  cnmptre  21531  iimulcn  21542  icchmeo  21545  xrhmeo  21550  cnheiborlem  21558  bndth  21562  evth  21563  evth2  21564  lebnumlem2  21566  lebnumlem3  21567  reparphti  21601  tchex  21764  tchnmfval  21775  fmcfil  21815  causs  21841  bcthlem5  21871  minveclem1  21943  minveclem3b  21947  evthicc2  21976  ovolficcss  21985  elovolm  21990  ovolmge0  21992  ovollb  21994  ovolgelb  21995  ovollb2lem  22003  ovollb2  22004  ovolunlem1a  22011  ovolunlem1  22012  ovoliunlem1  22017  ovoliunlem2  22018  ovoliun  22020  ovoliun2  22021  ovolscalem1  22028  ovolicc1  22031  ovolicc2lem4  22035  ovolicc2  22037  voliunlem2  22065  voliunlem3  22066  volsup  22070  ioombl1lem2  22073  ioombl1lem4  22075  uniioovol  22092  uniiccvol  22093  uniioombllem1  22094  uniioombllem2  22096  uniioombllem3  22098  uniioombllem6  22101  uniioombl  22102  dyadmbllem  22112  dyadmbl  22113  opnmbllem  22114  opnmblALT  22116  volsup2  22118  vitalilem2  22122  vitalilem4  22124  vitalilem5  22125  mbfconstlem  22140  mbfsup  22175  mbfinf  22176  mbflimsup  22177  i1fima  22189  i1fima2  22190  i1fd  22192  itg1cl  22196  itg1ge0  22197  i1f1  22201  itg11  22202  i1fmullem  22205  i1fadd  22206  i1fmul  22207  itg1addlem4  22210  itg1addlem5  22211  i1fmulc  22214  itg1mulc  22215  i1fres  22216  itg10a  22221  itg1ge0a  22222  itg1climres  22225  mbfi1fseqlem4  22229  itg2seq  22253  itg2monolem1  22261  itg2monolem2  22262  itg2monolem3  22263  itg2mono  22264  itg2i1fseq2  22267  itg2gt0  22271  itg2cnlem1  22272  itg2cn  22274  limciun  22402  c1liplem1  22501  dvne0  22516  dvne0f1  22517  lhop2  22520  dvcnvrelem2  22523  dvcnvre  22524  mdegleb  22568  mdeglt  22569  mdegldg  22570  mdegxrcl  22571  mdegcl  22573  ig1peu  22676  aalioulem3  22834  ulmss  22896  reeff1o  22946  efifo  23038  dvlog  23138  efopn  23145  logccv  23150  efrlim  23435  basellem3  23492  fsumvma  23624  lgseisenlem4  23763  dchrisum0fno1  23832  edgss  24494  frgrancvvdeqlem8  25182  ghsubgolemOLD  25510  ubthlem1  25924  minvecolem1  25928  htthlem  25972  hhssims  26329  shsss  26369  pjrni  26758  imaelshi  27114  foresf1o  27544  ofrn  27649  ofrn2  27650  fimarab  27653  xppreima2  27658  xrge0tsmsd  27960  locfinreflem  28028  cmpcref  28038  ordtrestNEW  28088  ordtrest2NEW  28090  xrge0mulc1cn  28108  rge0scvg  28116  esumcst  28242  esumpfinvallem  28253  esumpcvgval  28257  esumcvg  28265  esumiun  28273  omssubadd  28463  carsggect  28481  sibfinima  28500  sitgclg  28503  sitgclbn  28504  eulerpartgbij  28530  eulerpartlemgvv  28534  eulerpartlemgf  28537  rrvrnss  28605  orvcval4  28618  ballotlemsima  28673  lgamcvg2  28822  erdsze2lem2  28873  cvxpcon  28912  cvxscon  28913  cvmsss2  28944  cvmliftlem8  28962  cvmlift3lem6  28994  mrsubrn  29098  mrsubf  29102  msubrn  29114  msubf  29117  mstapst  29132  mvtss  29138  mclsssvlem  29147  mclsax  29154  mclsind  29155  mclsppslem  29168  ghomgrpilem2  29251  ghomfo  29256  orderseqlem  29533  norn  29612  heicant  30250  opnmbllem0  30251  mblfinlem1  30252  mblfinlem2  30253  mblfinlem3  30254  mblfinlem4  30255  ismblfin  30256  volsupnfl  30260  itg2addnclem2  30269  itg2gt0cn  30272  ftc1anclem3  30294  ftc1anclem5  30296  ftc1anclem6  30297  ftc1anclem7  30298  ftc1anclem8  30299  ftc1anc  30300  neibastop2lem  30380  tailfb  30397  indexdom  30427  cnresima  30462  istotbnd3  30469  sstotbnd2  30472  sstotbnd  30473  totbndbnd  30487  prdsbnd  30491  cntotbnd  30494  ismtyima  30501  heibor1lem  30507  heiborlem1  30509  heibor  30519  rrnval  30525  rrnequiv  30533  reheibor  30537  elrfirn  30829  cmpfiiin  30831  isnacs2  30840  isnacs3  30844  nacsfix  30846  coeq0i  30887  diophrw  30893  eldioph2lem2  30895  dnwech  31196  fnwe2lem2  31199  lmhmfgima  31232  pwssplit4  31237  hbt  31283  refsumcn  31608  cncmpmax  31610  climinf  31813  icccncfext  31891  dvsinax  31909  itgsubsticclem  31975  fourierdlem12  32102  fourierdlem42  32132  fourierdlem54  32144  fourierdlem70  32160  fourierdlem76  32166  fourierdlem82  32172  fourierdlem85  32175  fourierdlem88  32178  fourierdlem93  32183  fourierdlem113  32203  fafvelrn  32456  pfxrn  32603  mgmplusfreseq  32814  mgmhmima  32843  elbigolo1  33413  aacllem  33585  lsatset  35163  lsatlss  35169  cdleme50rnlem  36718  imo72b2lem0  38546  imo72b2lem2  38548  imo72b2lem1  38552  imo72b2  38557
  Copyright terms: Public domain W3C validator