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

Theorem frn 5598
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 5459 . 2  |-  ( F : A --> B  <->  ( F  Fn  A  /\  ran  F  C_  B ) )
21simprbi 452 1  |-  ( F : A --> B  ->  ran  F  C_  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    C_ wss 3321   ran crn 4880    Fn wfn 5450   -->wf 5451
This theorem is referenced by:  fco2  5602  fssxp  5603  fimacnvdisj  5622  f00  5629  foconst  5665  fun11iun  5696  fimacnv  5863  ffvelrn  5869  f1ompt  5892  fnfvrnss  5897  rnmptss  5898  f1dmex  5972  fliftrel  6031  isofr2  6065  fo1stres  6371  fo2ndres  6372  1stcof  6375  2ndcof  6376  fo2ndf  6454  fnwelem  6462  tposf2  6504  iunon  6601  iinon  6603  onoviun  6606  onnseq  6607  smores2  6617  seqomlem2  6709  oacomf1olem  6808  map0b  7053  mapsn  7056  f1imaen2g  7169  domdifsn  7192  domunsncan  7209  omxpenlem  7210  fodomr  7259  domss2  7267  f1finf1o  7336  f1fi  7394  unirnffid  7399  fissuni  7412  fipreima  7413  indexfi  7415  intrnfi  7422  dffi3  7437  ordtypelem8  7495  ordtypelem9  7496  ordtypelem10  7497  oismo  7510  hartogslem1  7512  brwdom2  7542  unxpwdom2  7557  ixpiunwdom  7560  infdifsn  7612  cantnf  7650  ac10ct  7916  numacn  7931  acndom  7933  acndom2  7936  infpwfien  7944  carduniima  7978  dfac12lem2  8025  dfac12lem3  8026  ackbij1  8119  fictb  8126  cfflb  8140  fin23lem40  8232  fin23lem41  8233  isf34lem5  8259  isf34lem7  8260  isf34lem6  8261  enfin1ai  8265  fin1a2lem6  8286  fin1a2lem7  8287  hsmexlem4  8310  hsmexlem5  8311  axdc2lem  8329  axdc3lem2  8332  ttukeylem6  8395  unirnfdomd  8443  pwcfsdom  8459  smobeth  8462  canthp1lem2  8529  pwfseqlem5  8539  wuncval2  8623  tskurn  8665  wfgru  8692  peano5nni  10004  rpnnen1lem4  10604  rpnnen1lem5  10605  unirnioo  11005  fseqsupcl  11317  fseqsupubi  11318  hashf1lem1  11705  hashf1lem2  11706  limsupcl  12268  limsupgle  12272  limsuple  12273  limsupval2  12275  limsupgre  12276  isercolllem2  12460  isercoll  12462  isercoll2  12463  climsup  12464  ruclem11  12840  prmreclem6  13290  4sqlem11  13324  vdwapf  13341  vdwlem11  13360  0ram  13389  0ram2  13390  0ramcl  13392  imasdsval2  13743  mrcssv  13840  isacs1i  13883  funcres2b  14095  funcres2c  14099  setcepi  14244  yoniso  14383  isacs4lem  14595  acsmapd  14605  acsmap2d  14606  mhmima  14764  gsumval1  14780  gsumwspan  14792  frmdss2  14809  cycsubgcl  14967  cycsubgss  14968  ghmrn  15020  conjnmz  15040  cntzmhm  15138  dfod2  15201  odcl2  15202  odf1o2  15208  sylow1lem2  15234  pgpssslw  15249  sylow2blem1  15255  lsmssv  15278  lsmidm  15297  pj1ghm2  15337  efgsp1  15370  efgsfo  15372  efgrelexlemb  15383  gexex  15469  iscyggen2  15492  cyggenod  15495  iscyg3  15497  gsumval3eu  15514  gsumval3  15515  cntzcmnf  15516  gsumzsubmcl  15524  gsumzaddlem  15527  gsumzadd  15528  gsumzsplit  15530  gsumconst  15533  gsumzoppg  15540  gsumpt  15546  dmdprdd  15561  dprdfcntz  15574  dprdfeq0  15581  dprdlub  15585  dprdres  15587  dprdss  15588  dprdz  15589  dprdf1  15592  subgdmdprd  15593  subgdprd  15594  dprd2dlem1  15600  dprd2da  15601  dmdprdsplit2lem  15604  dpjghm2  15623  ablfac1b  15629  lmhmlsp  16126  pj1lmhm2  16174  aspval2  16406  mplbas2  16532  mplind  16563  pjfo  16943  iinopn  16976  tgiun  17045  pptbas  17073  tgrest  17224  resttopon  17226  rest0  17234  restfpw  17244  ordtbaslem  17253  ordtuni  17255  ordtbas2  17256  ordtrest  17267  ordtrest2  17269  leordtval2  17277  lecldbas  17284  cnclsi  17337  cnrest  17350  cnrest2r  17352  cnprest2  17355  lmss  17363  cncmp  17456  rncmp  17460  discmp  17462  cmpsub  17464  tgcmp  17465  hauscmplem  17470  bwth  17474  conima  17489  concn  17490  2ndcctbss  17519  2ndcdisj  17520  2ndcomap  17522  2ndcsep  17523  dis2ndc  17524  lly1stc  17560  kgentop  17575  kgencmp  17578  1stckgenlem  17586  1stckgen  17587  kgencn2  17590  kgencn3  17591  txuni2  17598  ptbasfi  17614  xkoopn  17622  xkouni  17632  txbasval  17639  xkoccn  17652  ptcnplem  17654  upxp  17656  uptx  17658  txtube  17673  txcmplem1  17674  txcmplem2  17675  tx1stc  17683  txkgen  17685  xkoptsub  17687  xkoco1cn  17690  xkoco2cn  17691  xkococnlem  17692  xkococn  17693  xkoinjcn  17720  hmeores  17804  hmphdis  17829  fbasrn  17917  trfilss  17922  trfg  17924  zfbas  17929  uzrest  17930  elfm  17980  imaelfm  17984  rnelfmlem  17985  fclscmpi  18062  alexsublem  18076  alexsubALT  18083  ptcmplem1  18084  ptcmplem3  18086  cnextcn  18099  tmdgsum2  18127  symgtgp  18132  submtmd  18135  subgtgp  18136  subgntr  18137  opnsubg  18138  clsnsg  18140  tgpconcomp  18143  tsmsfbas  18158  tsmsxplem1  18183  prdsdsf  18398  prdsxmetlem  18399  prdsmet  18401  imasdsf1olem  18404  unirnblps  18450  unirnbl  18451  blin2  18460  imasf1oxms  18520  prdsbl  18522  met1stc  18552  met2ndci  18553  prdsxmslem2  18560  tgqioo  18832  xrtgioo  18838  xrge0gsumle  18865  xrge0tsms  18866  metdcn2  18871  metdsf  18879  metdsge  18880  metdscn2  18888  cnmptre  18953  iimulcn  18964  icchmeo  18967  xrhmeo  18972  cnheiborlem  18980  bndth  18984  evth  18985  evth2  18986  lebnumlem2  18988  lebnumlem3  18989  reparphti  19023  tchex  19177  tchnmfval  19187  fmcfil  19226  causs  19252  bcthlem5  19282  minveclem1  19326  minveclem3b  19330  evthicc2  19358  ovolficcss  19367  elovolm  19372  ovolmge0  19374  ovollb  19376  ovolgelb  19377  ovollb2lem  19385  ovollb2  19386  ovolunlem1a  19393  ovolunlem1  19394  ovoliunlem1  19399  ovoliunlem2  19400  ovoliun  19402  ovoliun2  19403  ovolscalem1  19410  ovolicc1  19413  ovolicc2lem4  19417  ovolicc2  19419  voliunlem2  19446  voliunlem3  19447  volsup  19451  ioombl1lem2  19454  ioombl1lem4  19456  uniioovol  19472  uniiccvol  19473  uniioombllem1  19474  uniioombllem2  19476  uniioombllem3  19478  uniioombllem6  19481  uniioombl  19482  dyadmbllem  19492  dyadmbl  19493  opnmbllem  19494  opnmblALT  19496  volsup2  19498  vitalilem2  19502  vitalilem4  19504  vitalilem5  19505  mbfconstlem  19522  mbfsup  19557  mbfinf  19558  mbflimsup  19559  i1fima  19571  i1fima2  19572  i1fd  19574  itg1cl  19578  itg1ge0  19579  i1f1  19583  itg11  19584  i1fmullem  19587  i1fadd  19588  i1fmul  19589  itg1addlem4  19592  itg1addlem5  19593  i1fmulc  19596  itg1mulc  19597  i1fres  19598  itg10a  19603  itg1ge0a  19604  itg1climres  19607  mbfi1fseqlem4  19611  itg2seq  19635  itg2monolem1  19643  itg2monolem2  19644  itg2monolem3  19645  itg2mono  19646  itg2i1fseq2  19649  itg2gt0  19653  itg2cnlem1  19654  itg2cn  19656  limciun  19782  c1liplem1  19881  dvne0  19896  dvne0f1  19897  lhop2  19900  dvcnvrelem2  19903  dvcnvre  19904  evlslem1  19937  evlseu  19938  mdegleb  19988  mdeglt  19989  mdegldg  19990  mdegxrcl  19991  mdegcl  19993  ig1peu  20095  aalioulem3  20252  ulmss  20314  reeff1o  20364  efifo  20450  dvlog  20543  efopn  20550  logccv  20555  efrlim  20809  basellem3  20866  fsumvma  20998  lgseisenlem4  21137  dchrisum0fno1  21206  ghsubgolem  21959  ubthlem1  22373  minvecolem1  22377  htthlem  22421  hhssims  22776  shsss  22816  pjrni  23205  imaelshi  23562  ofrn  24053  ofrn2  24054  xppreima2  24061  xrge0tsmsd  24224  xrge0mulc1cn  24328  rge0scvg  24336  esumcst  24456  esumpfinvallem  24465  esumpcvgval  24469  esumcvg  24477  sitgclg  24657  sitgclbn  24658  rrvrnss  24706  orvcval4  24719  ballotlemsima  24774  lgamcvg2  24840  erdsze2lem2  24891  cvxpcon  24930  cvxscon  24931  cvmsss2  24962  cvmliftlem8  24980  cvmlift3lem6  25012  ghomgrpilem2  25098  ghomfo  25103  orderseqlem  25528  norn  25607  opnmbllem0  26243  mblfinlem1  26244  mblfinlem2  26245  mblfinlem3  26246  mblfinlem4  26247  ismblfin  26248  volsupnfl  26252  itg2addnclem2  26258  itg2gt0cn  26261  ftc1anclem3  26283  ftc1anclem5  26285  ftc1anclem6  26286  ftc1anclem7  26287  ftc1anclem8  26288  ftc1anc  26289  comppfsc  26388  neibastop2lem  26390  tailfb  26407  indexdom  26437  cnresima  26474  istotbnd3  26481  sstotbnd2  26484  sstotbnd  26485  totbndbnd  26499  prdsbnd  26503  cntotbnd  26506  ismtyima  26513  heibor1lem  26519  heiborlem1  26521  heibor  26531  rrnval  26537  rrnequiv  26545  reheibor  26549  elrfirn  26750  cmpfiiin  26752  isnacs2  26761  isnacs3  26765  nacsfix  26767  coeq0i  26812  diophrw  26818  eldioph2lem2  26820  dnwech  27124  fnwe2lem2  27127  lmhmfgima  27160  pwssplit4  27169  frlmsplit2  27221  frlmsslsp  27226  frlmlbs  27227  frlmup3  27230  frlmup4  27231  lindff1  27268  lindfrn  27269  f1lindf  27270  lindfmm  27275  indlcim  27288  hbt  27312  f1omvdconj  27367  psgnunilem1  27394  refsumcn  27678  cncmpmax  27680  climinf  27709  fafvelrn  28011  hashimarn  28164  frgrancvvdeqlem8  28430  lsatset  29789  lsatlss  29795  cdleme50rnlem  31342
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 179  df-an 362  df-f 5459
  Copyright terms: Public domain W3C validator