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

Theorem frn 5564
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 5425 . 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 3288   ran crn 4846    Fn wfn 5416   -->wf 5417
This theorem is referenced by:  fco2  5568  fssxp  5569  fimacnvdisj  5588  f00  5595  foconst  5631  fun11iun  5662  fimacnv  5829  ffvelrn  5835  f1ompt  5858  fnfvrnss  5863  rnmptss  5864  f1dmex  5938  fliftrel  5997  isofr2  6031  fo1stres  6337  fo2ndres  6338  1stcof  6341  2ndcof  6342  fo2ndf  6420  fnwelem  6428  tposf2  6470  iunon  6567  iinon  6569  onoviun  6572  onnseq  6573  smores2  6583  seqomlem2  6675  oacomf1olem  6774  map0b  7019  mapsn  7022  f1imaen2g  7135  domdifsn  7158  domunsncan  7175  omxpenlem  7176  fodomr  7225  domss2  7233  f1finf1o  7302  f1fi  7360  unirnffid  7364  fissuni  7377  fipreima  7378  indexfi  7380  intrnfi  7387  dffi3  7402  ordtypelem8  7458  ordtypelem9  7459  ordtypelem10  7460  oismo  7473  hartogslem1  7475  brwdom2  7505  unxpwdom2  7520  ixpiunwdom  7523  infdifsn  7575  cantnf  7613  ac10ct  7879  numacn  7894  acndom  7896  acndom2  7899  infpwfien  7907  carduniima  7941  dfac12lem2  7988  dfac12lem3  7989  ackbij1  8082  fictb  8089  cfflb  8103  fin23lem40  8195  fin23lem41  8196  isf34lem5  8222  isf34lem7  8223  isf34lem6  8224  enfin1ai  8228  fin1a2lem6  8249  fin1a2lem7  8250  hsmexlem4  8273  hsmexlem5  8274  axdc2lem  8292  axdc3lem2  8295  ttukeylem6  8358  unirnfdomd  8406  pwcfsdom  8422  smobeth  8425  canthp1lem2  8492  pwfseqlem5  8502  wuncval2  8586  tskurn  8628  wfgru  8655  peano5nni  9967  rpnnen1lem4  10567  rpnnen1lem5  10568  unirnioo  10968  fseqsupcl  11279  fseqsupubi  11280  hashf1lem1  11667  hashf1lem2  11668  limsupcl  12230  limsupgle  12234  limsuple  12235  limsupval2  12237  limsupgre  12238  isercolllem2  12422  isercoll  12424  isercoll2  12425  climsup  12426  ruclem11  12802  prmreclem6  13252  4sqlem11  13286  vdwapf  13303  vdwlem11  13322  0ram  13351  0ram2  13352  0ramcl  13354  imasdsval2  13705  mrcssv  13802  isacs1i  13845  funcres2b  14057  funcres2c  14061  setcepi  14206  yoniso  14345  isacs4lem  14557  acsmapd  14567  acsmap2d  14568  mhmima  14726  gsumval1  14742  gsumwspan  14754  frmdss2  14771  cycsubgcl  14929  cycsubgss  14930  ghmrn  14982  conjnmz  15002  cntzmhm  15100  dfod2  15163  odcl2  15164  odf1o2  15170  sylow1lem2  15196  pgpssslw  15211  sylow2blem1  15217  lsmssv  15240  lsmidm  15259  pj1ghm2  15299  efgsp1  15332  efgsfo  15334  efgrelexlemb  15345  gexex  15431  iscyggen2  15454  cyggenod  15457  iscyg3  15459  gsumval3eu  15476  gsumval3  15477  cntzcmnf  15478  gsumzsubmcl  15486  gsumzaddlem  15489  gsumzadd  15490  gsumzsplit  15492  gsumconst  15495  gsumzoppg  15502  gsumpt  15508  dmdprdd  15523  dprdfcntz  15536  dprdfeq0  15543  dprdlub  15547  dprdres  15549  dprdss  15550  dprdz  15551  dprdf1  15554  subgdmdprd  15555  subgdprd  15556  dprd2dlem1  15562  dprd2da  15563  dmdprdsplit2lem  15566  dpjghm2  15585  ablfac1b  15591  lmhmlsp  16088  pj1lmhm2  16136  aspval2  16368  mplbas2  16494  mplind  16525  pjfo  16905  iinopn  16938  tgiun  17007  pptbas  17035  tgrest  17185  resttopon  17187  rest0  17195  restfpw  17205  ordtbaslem  17214  ordtuni  17216  ordtbas2  17217  ordtrest  17228  ordtrest2  17230  leordtval2  17238  lecldbas  17245  cnclsi  17298  cnrest  17311  cnrest2r  17313  cnprest2  17316  lmss  17324  cncmp  17417  rncmp  17421  discmp  17423  cmpsub  17425  tgcmp  17426  hauscmplem  17431  conima  17449  concn  17450  2ndcctbss  17479  2ndcdisj  17480  2ndcomap  17482  2ndcsep  17483  dis2ndc  17484  lly1stc  17520  kgentop  17535  kgencmp  17538  1stckgenlem  17546  1stckgen  17547  kgencn2  17550  kgencn3  17551  txuni2  17558  ptbasfi  17574  xkoopn  17582  xkouni  17592  txbasval  17599  xkoccn  17612  ptcnplem  17614  upxp  17616  uptx  17618  txtube  17633  txcmplem1  17634  txcmplem2  17635  tx1stc  17643  txkgen  17645  xkoptsub  17647  xkoco1cn  17650  xkoco2cn  17651  xkococnlem  17652  xkococn  17653  xkoinjcn  17680  hmeores  17764  hmphdis  17789  fbasrn  17877  trfilss  17882  trfg  17884  zfbas  17889  uzrest  17890  elfm  17940  imaelfm  17944  rnelfmlem  17945  fclscmpi  18022  alexsublem  18036  alexsubALT  18043  ptcmplem1  18044  ptcmplem3  18046  cnextcn  18059  tmdgsum2  18087  symgtgp  18092  submtmd  18095  subgtgp  18096  subgntr  18097  opnsubg  18098  clsnsg  18100  tgpconcomp  18103  tsmsfbas  18118  tsmsxplem1  18143  prdsdsf  18358  prdsxmetlem  18359  prdsmet  18361  imasdsf1olem  18364  unirnblps  18410  unirnbl  18411  blin2  18420  imasf1oxms  18480  prdsbl  18482  met1stc  18512  met2ndci  18513  prdsxmslem2  18520  tgqioo  18792  xrtgioo  18798  xrge0gsumle  18825  xrge0tsms  18826  metdcn2  18831  metdsf  18839  metdsge  18840  metdscn2  18848  cnmptre  18913  iimulcn  18924  icchmeo  18927  xrhmeo  18932  cnheiborlem  18940  bndth  18944  evth  18945  evth2  18946  lebnumlem2  18948  lebnumlem3  18949  reparphti  18983  tchex  19137  tchnmfval  19147  fmcfil  19186  causs  19212  bcthlem5  19242  minveclem1  19286  minveclem3b  19290  evthicc2  19318  ovolficcss  19327  elovolm  19332  ovolmge0  19334  ovollb  19336  ovolgelb  19337  ovollb2lem  19345  ovollb2  19346  ovolunlem1a  19353  ovolunlem1  19354  ovoliunlem1  19359  ovoliunlem2  19360  ovoliun  19362  ovoliun2  19363  ovolscalem1  19370  ovolicc1  19373  ovolicc2lem4  19377  ovolicc2  19379  voliunlem2  19406  voliunlem3  19407  volsup  19411  ioombl1lem2  19414  ioombl1lem4  19416  uniioovol  19432  uniiccvol  19433  uniioombllem1  19434  uniioombllem2  19436  uniioombllem3  19438  uniioombllem6  19441  uniioombl  19442  dyadmbllem  19452  dyadmbl  19453  opnmbllem  19454  opnmblALT  19456  volsup2  19458  vitalilem2  19462  vitalilem4  19464  vitalilem5  19465  mbfconstlem  19482  mbfsup  19517  mbfinf  19518  mbflimsup  19519  i1fima  19531  i1fima2  19532  i1fd  19534  itg1cl  19538  itg1ge0  19539  i1f1  19543  itg11  19544  i1fmullem  19547  i1fadd  19548  i1fmul  19549  itg1addlem4  19552  itg1addlem5  19553  i1fmulc  19556  itg1mulc  19557  i1fres  19558  itg10a  19563  itg1ge0a  19564  itg1climres  19567  mbfi1fseqlem4  19571  itg2seq  19595  itg2monolem1  19603  itg2monolem2  19604  itg2monolem3  19605  itg2mono  19606  itg2i1fseq2  19609  itg2gt0  19613  itg2cnlem1  19614  itg2cn  19616  limciun  19742  c1liplem1  19841  dvne0  19856  dvne0f1  19857  lhop2  19860  dvcnvrelem2  19863  dvcnvre  19864  evlslem1  19897  evlseu  19898  mdegleb  19948  mdeglt  19949  mdegldg  19950  mdegxrcl  19951  mdegcl  19953  ig1peu  20055  aalioulem3  20212  ulmss  20274  reeff1o  20324  efifo  20410  dvlog  20503  efopn  20510  logccv  20515  efrlim  20769  basellem3  20826  fsumvma  20958  lgseisenlem4  21097  dchrisum0fno1  21166  ghsubgolem  21919  ubthlem1  22333  minvecolem1  22337  htthlem  22381  hhssims  22736  shsss  22776  pjrni  23165  imaelshi  23522  ofrn  24013  ofrn2  24014  xppreima2  24021  xrge0tsmsd  24184  xrge0mulc1cn  24288  rge0scvg  24296  esumcst  24416  esumpfinvallem  24425  esumpcvgval  24429  esumcvg  24437  sitgclg  24617  sitgclbn  24618  rrvrnss  24666  orvcval4  24679  ballotlemsima  24734  lgamcvg2  24800  erdsze2lem2  24851  cvxpcon  24890  cvxscon  24891  cvmsss2  24922  cvmliftlem8  24940  cvmlift3lem6  24972  ghomgrpilem2  25058  ghomfo  25063  orderseqlem  25474  norn  25527  mblfinlem  26151  mblfinlem2  26152  mblfinlem3  26153  ismblfin  26154  volsupnfl  26158  itg2addnclem2  26164  itg2gt0cn  26167  comppfsc  26285  neibastop2lem  26287  tailfb  26304  indexdom  26334  cnresima  26371  istotbnd3  26378  sstotbnd2  26381  sstotbnd  26382  totbndbnd  26396  prdsbnd  26400  cntotbnd  26403  ismtyima  26410  heibor1lem  26416  heiborlem1  26418  heibor  26428  rrnval  26434  rrnequiv  26442  reheibor  26446  elrfirn  26647  cmpfiiin  26649  isnacs2  26658  isnacs3  26662  nacsfix  26664  coeq0i  26709  diophrw  26715  eldioph2lem2  26717  dnwech  27021  fnwe2lem2  27024  lmhmfgima  27058  pwssplit4  27067  frlmsplit2  27119  frlmsslsp  27124  frlmlbs  27125  frlmup3  27128  frlmup4  27129  lindff1  27166  lindfrn  27167  f1lindf  27168  lindfmm  27173  indlcim  27186  hbt  27210  f1omvdconj  27265  psgnunilem1  27292  refsumcn  27576  cncmpmax  27578  climinf  27607  fafvelrn  27909  hashimarn  28002  frgrancvvdeqlem8  28151  lsatset  29485  lsatlss  29491  cdleme50rnlem  31038
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 5425
  Copyright terms: Public domain W3C validator