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

Theorem frn 5397
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 5261 . 2  |-  ( F : A --> B  <->  ( F  Fn  A  /\  ran  F  C_  B ) )
21simprbi 450 1  |-  ( F : A --> B  ->  ran  F  C_  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    C_ wss 3154   ran crn 4692    Fn wfn 5252   -->wf 5253
This theorem is referenced by:  fco2  5401  fssxp  5402  fimacnvdisj  5421  f00  5428  foconst  5464  fun11iun  5495  fimacnv  5659  ffvelrn  5665  f1ompt  5684  fnfvrnss  5689  f1dmex  5753  fliftrel  5809  isofr2  5843  fo1stres  6145  fo2ndres  6146  1stcof  6149  2ndcof  6150  fnwelem  6232  tposf2  6260  iunon  6357  iinon  6359  onoviun  6362  onnseq  6363  smores2  6373  seqomlem2  6465  oacomf1olem  6564  map0b  6808  mapsn  6811  f1imaen2g  6924  domdifsn  6947  domunsncan  6964  omxpenlem  6965  fodomr  7014  domss2  7022  f1finf1o  7088  f1fi  7145  unirnffid  7149  fissuni  7162  fipreima  7163  indexfi  7165  intrnfi  7172  dffi3  7186  ordtypelem8  7242  ordtypelem9  7243  ordtypelem10  7244  oismo  7257  hartogslem1  7259  brwdom2  7289  unxpwdom2  7304  ixpiunwdom  7307  infdifsn  7359  cantnf  7397  ac10ct  7663  numacn  7678  acndom  7680  acndom2  7683  infpwfien  7691  carduniima  7725  dfac12lem2  7772  dfac12lem3  7773  ackbij1  7866  fictb  7873  cfflb  7887  fin23lem40  7979  fin23lem41  7980  isf34lem5  8006  isf34lem7  8007  isf34lem6  8008  enfin1ai  8012  fin1a2lem6  8033  fin1a2lem7  8034  hsmexlem4  8057  hsmexlem5  8058  axdc2lem  8076  axdc3lem2  8079  ttukeylem6  8143  unirnfdomd  8191  pwcfsdom  8207  smobeth  8210  canthp1lem2  8277  pwfseqlem5  8287  wuncval2  8371  tskurn  8413  wfgru  8440  peano5nni  9751  rpnnen1lem4  10347  rpnnen1lem5  10348  unirnioo  10745  fseqsupcl  11041  fseqsupubi  11042  hashf1lem1  11395  hashf1lem2  11396  limsupcl  11949  limsupgle  11953  limsuple  11954  limsupval2  11956  limsupgre  11957  isercolllem2  12141  isercoll  12143  isercoll2  12144  climsup  12145  ruclem11  12520  prmreclem6  12970  4sqlem11  13004  vdwapf  13021  vdwlem11  13040  0ram  13069  0ram2  13070  0ramcl  13072  imasdsval2  13421  mrcssv  13518  isacs1i  13561  funcres2b  13773  funcres2c  13777  setcepi  13922  yoniso  14061  isacs4lem  14273  acsmapd  14283  acsmap2d  14284  mhmima  14442  gsumval1  14458  gsumwspan  14470  frmdss2  14487  cycsubgcl  14645  cycsubgss  14646  ghmrn  14698  conjnmz  14718  cntzmhm  14816  dfod2  14879  odcl2  14880  odf1o2  14886  sylow1lem2  14912  pgpssslw  14927  sylow2blem1  14933  lsmssv  14956  lsmidm  14975  pj1ghm2  15015  efgsp1  15048  efgsfo  15050  efgrelexlemb  15061  gexex  15147  iscyggen2  15170  cyggenod  15173  iscyg3  15175  gsumval3eu  15192  gsumval3  15193  cntzcmnf  15194  gsumzsubmcl  15202  gsumzaddlem  15205  gsumzadd  15206  gsumzsplit  15208  gsumconst  15211  gsumzoppg  15218  gsumpt  15224  dmdprdd  15239  dprdfcntz  15252  dprdfeq0  15259  dprdlub  15263  dprdres  15265  dprdss  15266  dprdz  15267  dprdf1  15270  subgdmdprd  15271  subgdprd  15272  dprd2dlem1  15278  dprd2da  15279  dmdprdsplit2lem  15282  dpjghm2  15301  ablfac1b  15307  lmhmlsp  15808  pj1lmhm2  15856  aspval2  16088  mplbas2  16214  mplind  16245  pjfo  16617  iinopn  16650  tgiun  16719  pptbas  16747  tgrest  16892  resttopon  16894  rest0  16902  restfpw  16912  ordtbaslem  16920  ordtuni  16922  ordtbas2  16923  ordtrest  16934  ordtrest2  16936  leordtval2  16944  lecldbas  16951  cnclsi  17003  cnrest  17015  cnrest2r  17017  cnprest2  17020  lmss  17028  cncmp  17121  rncmp  17125  discmp  17127  cmpsub  17129  tgcmp  17130  hauscmplem  17135  conima  17153  concn  17154  2ndcctbss  17183  2ndcdisj  17184  2ndcomap  17186  2ndcsep  17187  dis2ndc  17188  lly1stc  17224  kgentop  17239  kgencmp  17242  1stckgenlem  17250  1stckgen  17251  kgencn2  17254  kgencn3  17255  txuni2  17262  ptbasfi  17278  xkoopn  17286  xkouni  17296  txbasval  17303  xkoccn  17315  ptcnplem  17317  upxp  17319  uptx  17321  txtube  17336  txcmplem1  17337  txcmplem2  17338  tx1stc  17346  txkgen  17348  xkoptsub  17350  xkoco1cn  17353  xkoco2cn  17354  xkococnlem  17355  xkococn  17356  xkoinjcn  17383  hmeores  17464  hmphdis  17489  fbasrn  17581  trfilss  17586  trfg  17588  zfbas  17593  uzrest  17594  elfm  17644  imaelfm  17648  rnelfmlem  17649  fclscmpi  17726  alexsublem  17740  alexsubALT  17747  ptcmplem1  17748  ptcmplem3  17750  tmdgsum2  17781  symgtgp  17786  submtmd  17789  subgtgp  17790  subgntr  17791  opnsubg  17792  clsnsg  17794  tgpconcomp  17797  tsmsfbas  17812  tsmsxplem1  17837  prdsdsf  17933  prdsxmetlem  17934  prdsmet  17936  imasdsf1olem  17939  unirnbl  17971  blin2  17977  imasf1oxms  18037  prdsbl  18039  met1stc  18069  met2ndci  18070  prdsxmslem2  18077  tgqioo  18308  xrtgioo  18314  xrge0gsumle  18340  xrge0tsms  18341  metdcn2  18346  metdsf  18354  metdsge  18355  metdscn2  18363  cnmptre  18427  iimulcn  18438  icchmeo  18441  xrhmeo  18446  cnheiborlem  18454  bndth  18458  evth  18459  evth2  18460  lebnumlem2  18462  lebnumlem3  18463  reparphti  18497  tchex  18651  tchnmfval  18661  fmcfil  18700  causs  18726  bcthlem5  18752  minveclem1  18790  minveclem3b  18794  evthicc2  18822  ovolficcss  18831  elovolm  18836  ovolmge0  18838  ovollb  18840  ovolgelb  18841  ovollb2lem  18849  ovollb2  18850  ovolunlem1a  18857  ovolunlem1  18858  ovoliunlem1  18863  ovoliunlem2  18864  ovoliun  18866  ovoliun2  18867  ovolscalem1  18874  ovolicc1  18877  ovolicc2lem4  18881  ovolicc2  18883  voliunlem2  18910  voliunlem3  18911  volsup  18915  ioombl1lem2  18918  ioombl1lem4  18920  uniioovol  18936  uniiccvol  18937  uniioombllem1  18938  uniioombllem2  18940  uniioombllem3  18942  uniioombllem6  18945  uniioombl  18946  dyadmbllem  18956  dyadmbl  18957  opnmbllem  18958  opnmblALT  18960  volsup2  18962  vitalilem2  18966  vitalilem4  18968  vitalilem5  18969  mbfconstlem  18986  mbfsup  19021  mbfinf  19022  mbflimsup  19023  i1fima  19035  i1fima2  19036  i1fd  19038  itg1cl  19042  itg1ge0  19043  i1f1  19047  itg11  19048  i1fmullem  19051  i1fadd  19052  i1fmul  19053  itg1addlem4  19056  itg1addlem5  19057  i1fmulc  19060  itg1mulc  19061  i1fres  19062  itg10a  19067  itg1ge0a  19068  itg1climres  19071  mbfi1fseqlem4  19075  itg2seq  19099  itg2monolem1  19107  itg2monolem2  19108  itg2monolem3  19109  itg2mono  19110  itg2i1fseq2  19113  itg2gt0  19117  itg2cnlem1  19118  itg2cn  19120  limciun  19246  c1liplem1  19345  dvne0  19360  dvne0f1  19361  lhop2  19364  dvcnvrelem2  19367  dvcnvre  19368  evlslem1  19401  evlseu  19402  mdegleb  19452  mdeglt  19453  mdegldg  19454  mdegxrcl  19455  mdegcl  19457  ig1peu  19559  aalioulem3  19716  ulmss  19776  reeff1o  19825  efifo  19911  dvlog  20000  efopn  20007  logccv  20012  efrlim  20266  basellem3  20322  fsumvma  20454  lgseisenlem4  20593  dchrisum0fno1  20662  ghsubgolem  21039  ubthlem1  21451  minvecolem1  21455  htthlem  21499  hhssims  21854  shsss  21894  pjrni  22283  imaelshi  22640  ballotlemsima  23076  ofrn  23208  ofrn2  23209  xppreima2  23214  rnmptss  23240  xrge0mulc1cn  23325  rge0scvg  23375  xrge0tsmsd  23384  esumcst  23438  esumpfinvallem  23444  esumpcvgval  23448  esumcvg  23456  rrvrnss  23652  orvcval4  23663  erdsze2lem2  23737  cvxpcon  23775  cvxscon  23776  cvmsss2  23807  cvmliftlem8  23825  cvmlift3lem6  23857  ghomgrpilem2  23995  ghomfo  24000  orderseqlem  24254  norn  24307  itg2addnclem2  24934  basexre  25533  cmptdst  25579  limptlimpr2lem2  25586  bwt2  25603  supnuf  25640  supbrr  25647  rdmob  25759  rcmob  25760  comppfsc  26318  neibastop2lem  26320  tailfb  26337  indexdom  26424  cnresima  26495  istotbnd3  26506  sstotbnd2  26509  sstotbnd  26510  totbndbnd  26524  prdsbnd  26528  cntotbnd  26531  ismtyima  26538  heibor1lem  26544  heiborlem1  26546  heibor  26556  rrnval  26562  rrnequiv  26570  reheibor  26574  elrfirn  26781  cmpfiiin  26783  isnacs2  26792  isnacs3  26796  nacsfix  26798  coeq0i  26843  diophrw  26849  eldioph2lem2  26851  dnwech  27156  fnwe2lem2  27159  lmhmfgima  27193  pwssplit4  27202  frlmsplit2  27254  frlmsslsp  27259  frlmlbs  27260  frlmup3  27263  frlmup4  27264  lindff1  27301  lindfrn  27302  f1lindf  27303  lindfmm  27308  indlcim  27321  hbt  27345  f1omvdconj  27400  psgnunilem1  27427  fnvinran  27696  refsumcn  27712  cncmpmax  27714  climinf  27743  fafvelrn  28043  lsatset  29253  lsatlss  29259  cdleme50rnlem  30806
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 177  df-an 360  df-f 5261
  Copyright terms: Public domain W3C validator