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

Theorem frn 5735
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 5590 . 2  |-  ( F : A --> B  <->  ( F  Fn  A  /\  ran  F  C_  B ) )
21simprbi 464 1  |-  ( F : A --> B  ->  ran  F  C_  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    C_ wss 3476   ran crn 5000    Fn wfn 5581   -->wf 5582
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 371  df-f 5590
This theorem is referenced by:  fco2  5740  fssxp  5741  fimacnvdisj  5761  f00  5765  f0rn0  5768  foconst  5804  fimacnv  6011  ffvelrn  6017  f1ompt  6041  fnfvrnss  6047  rnmptss  6048  fliftrel  6192  isofr2  6226  fun11iun  6741  f1dmex  6751  fo1stres  6805  fo2ndres  6806  1stcof  6809  2ndcof  6810  fo2ndf  6887  fnwelem  6895  tposf2  6976  iunon  7006  iinon  7008  onoviun  7011  onnseq  7012  smores2  7022  seqomlem2  7113  oacomf1olem  7210  map0b  7454  mapsn  7457  f1imaen2g  7573  domdifsn  7597  domunsncan  7614  omxpenlem  7615  fodomr  7665  domss2  7673  f1finf1o  7743  f1fi  7803  unirnffid  7808  fissuni  7821  fipreima  7822  indexfi  7824  intrnfi  7872  dffi3  7887  ordtypelem8  7946  ordtypelem9  7947  ordtypelem10  7948  oismo  7961  hartogslem1  7963  brwdom2  7995  unxpwdom2  8010  ixpiunwdom  8013  infdifsn  8069  cantnf  8108  cantnfOLD  8130  ac10ct  8411  numacn  8426  acndom  8428  acndom2  8431  infpwfien  8439  carduniima  8473  dfac12lem2  8520  dfac12lem3  8521  ackbij1  8614  fictb  8621  cfflb  8635  fin23lem40  8727  fin23lem41  8728  isf34lem5  8754  isf34lem7  8755  isf34lem6  8756  enfin1ai  8760  fin1a2lem6  8781  fin1a2lem7  8782  hsmexlem4  8805  hsmexlem5  8806  axdc2lem  8824  axdc3lem2  8827  ttukeylem6  8890  unirnfdomd  8938  pwcfsdom  8954  smobeth  8957  canthp1lem2  9027  pwfseqlem5  9037  wuncval2  9121  tskurn  9163  wfgru  9190  peano5nni  10535  rpnnen1lem4  11207  rpnnen1lem5  11208  unirnioo  11620  fseqsupcl  12051  fseqsupubi  12052  hashimarn  12458  hashf1lem1  12466  hashf1lem2  12467  swrdrn  12613  cshwrn  12732  limsupcl  13255  limsupgle  13259  limsuple  13260  limsupval2  13262  limsupgre  13263  isercolllem2  13447  isercoll  13449  isercoll2  13450  climsup  13451  ruclem11  13830  prmreclem6  14294  4sqlem11  14328  vdwapf  14345  vdwlem11  14364  0ram  14393  0ram2  14394  0ramcl  14396  imasdsval2  14767  mrcssv  14865  isacs1i  14908  funcres2b  15120  funcres2c  15124  setcepi  15269  yoniso  15408  isacs4lem  15651  acsmapd  15661  acsmap2d  15662  mhmima  15804  gsumval1  15822  gsumwspan  15837  frmdss2  15854  cycsubgcl  16022  cycsubgss  16023  ghmrn  16075  conjnmz  16095  cntzmhm  16171  f1omvdconj  16267  psgnunilem1  16314  dfod2  16382  odcl2  16383  odf1o2  16389  sylow1lem2  16415  pgpssslw  16430  sylow2blem1  16436  lsmssv  16459  lsmidm  16478  pj1ghm2  16518  efgsp1  16551  efgsfo  16553  efgrelexlemb  16564  cntzcmnf  16644  gexex  16652  iscyggen2  16675  cyggenod  16678  iscyg3  16680  gsumval3eu  16698  gsumval3OLD  16699  gsumval3lem1  16700  gsumval3lem2  16701  gsumval3  16702  gsumzsubmcl  16719  gsumzsubmclOLD  16720  gsumzaddlem  16725  gsumzadd  16726  gsumzaddlemOLD  16727  gsumzaddOLD  16728  gsumzsplit  16735  gsumzsplitOLD  16736  gsumconst  16745  gsumzoppg  16758  gsumzoppgOLD  16759  gsumpt  16779  gsumptOLD  16780  dmdprdd  16821  dprdfcntz  16839  dprdfcntzOLD  16845  dprdfeq0  16852  dprdfeq0OLD  16859  dprdlub  16863  dprdres  16865  dprdss  16866  dprdz  16867  dprdf1  16870  subgdmdprd  16871  subgdprd  16872  dprd2dlem1  16880  dprd2da  16881  dmdprdsplit2lem  16884  dpjghm2  16903  ablfac1b  16911  lmhmlsp  17478  pj1lmhm2  17530  aspval2  17767  mplcoe5lem  17901  mplbas2  17905  mplbas2OLD  17906  mplind  17938  evlslem1  17955  evlseu  17956  gsumply1subr  18046  pjfo  18513  frlmsplit2  18570  frlmsslsp  18596  frlmsslspOLD  18597  frlmlbs  18598  frlmup3  18601  frlmup4  18602  lindff1  18622  lindfrn  18623  f1lindf  18624  lindfmm  18629  indlcim  18642  m2cpmf1  19011  m2cpmghm  19012  m2cpmmhm  19013  iinopn  19178  tgiun  19247  pptbas  19275  tgrest  19426  resttopon  19428  rest0  19436  restfpw  19446  ordtbaslem  19455  ordtuni  19457  ordtbas2  19458  ordtrest  19469  ordtrest2  19471  leordtval2  19479  lecldbas  19486  cnclsi  19539  cnrest  19552  cnrest2r  19554  cnprest2  19557  lmss  19565  cncmp  19658  rncmp  19662  discmp  19664  cmpsub  19666  tgcmp  19667  hauscmplem  19672  bwthOLD  19677  conima  19692  concn  19693  2ndcctbss  19722  2ndcdisj  19723  2ndcomap  19725  2ndcsep  19726  dis2ndc  19727  lly1stc  19763  kgentop  19778  kgencmp  19781  1stckgenlem  19789  1stckgen  19790  kgencn2  19793  kgencn3  19794  txuni2  19801  ptbasfi  19817  xkoopn  19825  xkouni  19835  txbasval  19842  xkoccn  19855  ptcnplem  19857  upxp  19859  uptx  19861  txtube  19876  txcmplem1  19877  txcmplem2  19878  tx1stc  19886  txkgen  19888  xkoptsub  19890  xkoco1cn  19893  xkoco2cn  19894  xkococnlem  19895  xkococn  19896  xkoinjcn  19923  hmeores  20007  hmphdis  20032  fbasrn  20120  trfilss  20125  trfg  20127  zfbas  20132  uzrest  20133  elfm  20183  imaelfm  20187  rnelfmlem  20188  fclscmpi  20265  alexsublem  20279  alexsubALT  20286  ptcmplem1  20287  ptcmplem3  20289  cnextcn  20302  tmdgsum2  20330  symgtgp  20335  submtmd  20338  subgtgp  20339  subgntr  20340  opnsubg  20341  clsnsg  20343  tgpconcomp  20346  tsmsfbas  20361  tsmsxplem1  20390  prdsdsf  20605  prdsxmetlem  20606  prdsmet  20608  imasdsf1olem  20611  unirnblps  20657  unirnbl  20658  blin2  20667  imasf1oxms  20727  prdsbl  20729  met1stc  20759  met2ndci  20760  prdsxmslem2  20767  tgqioo  21040  xrtgioo  21046  xrge0gsumle  21073  xrge0tsms  21074  metdcn2  21079  metdsf  21087  metdsge  21088  metdscn2  21096  cnmptre  21162  iimulcn  21173  icchmeo  21176  xrhmeo  21181  cnheiborlem  21189  bndth  21193  evth  21194  evth2  21195  lebnumlem2  21197  lebnumlem3  21198  reparphti  21232  tchex  21395  tchnmfval  21406  fmcfil  21446  causs  21472  bcthlem5  21502  minveclem1  21574  minveclem3b  21578  evthicc2  21607  ovolficcss  21616  elovolm  21621  ovolmge0  21623  ovollb  21625  ovolgelb  21626  ovollb2lem  21634  ovollb2  21635  ovolunlem1a  21642  ovolunlem1  21643  ovoliunlem1  21648  ovoliunlem2  21649  ovoliun  21651  ovoliun2  21652  ovolscalem1  21659  ovolicc1  21662  ovolicc2lem4  21666  ovolicc2  21668  voliunlem2  21696  voliunlem3  21697  volsup  21701  ioombl1lem2  21704  ioombl1lem4  21706  uniioovol  21723  uniiccvol  21724  uniioombllem1  21725  uniioombllem2  21727  uniioombllem3  21729  uniioombllem6  21732  uniioombl  21733  dyadmbllem  21743  dyadmbl  21744  opnmbllem  21745  opnmblALT  21747  volsup2  21749  vitalilem2  21753  vitalilem4  21755  vitalilem5  21756  mbfconstlem  21771  mbfsup  21806  mbfinf  21807  mbflimsup  21808  i1fima  21820  i1fima2  21821  i1fd  21823  itg1cl  21827  itg1ge0  21828  i1f1  21832  itg11  21833  i1fmullem  21836  i1fadd  21837  i1fmul  21838  itg1addlem4  21841  itg1addlem5  21842  i1fmulc  21845  itg1mulc  21846  i1fres  21847  itg10a  21852  itg1ge0a  21853  itg1climres  21856  mbfi1fseqlem4  21860  itg2seq  21884  itg2monolem1  21892  itg2monolem2  21893  itg2monolem3  21894  itg2mono  21895  itg2i1fseq2  21898  itg2gt0  21902  itg2cnlem1  21903  itg2cn  21905  limciun  22033  c1liplem1  22132  dvne0  22147  dvne0f1  22148  lhop2  22151  dvcnvrelem2  22154  dvcnvre  22155  mdegleb  22199  mdeglt  22200  mdegldg  22201  mdegxrcl  22202  mdegcl  22204  ig1peu  22307  aalioulem3  22464  ulmss  22526  reeff1o  22576  efifo  22667  dvlog  22760  efopn  22767  logccv  22772  efrlim  23027  basellem3  23084  fsumvma  23216  lgseisenlem4  23355  dchrisum0fno1  23424  edgss  24028  frgrancvvdeqlem8  24717  ghsubgolem  25048  ubthlem1  25462  minvecolem1  25466  htthlem  25510  hhssims  25867  shsss  25907  pjrni  26296  imaelshi  26653  ofrn  27152  ofrn2  27153  xppreima2  27160  xrge0tsmsd  27438  ordtrestNEW  27539  ordtrest2NEW  27541  xrge0mulc1cn  27559  rge0scvg  27567  esumcst  27711  esumpfinvallem  27720  esumpcvgval  27724  esumcvg  27732  sibfinima  27921  sitgclg  27924  sitgclbn  27925  eulerpartgbij  27951  eulerpartlemgvv  27955  eulerpartlemgf  27958  rrvrnss  28026  orvcval4  28039  ballotlemsima  28094  lgamcvg2  28237  erdsze2lem2  28288  cvxpcon  28327  cvxscon  28328  cvmsss2  28359  cvmliftlem8  28377  cvmlift3lem6  28409  ghomgrpilem2  28501  ghomfo  28506  orderseqlem  28909  norn  28988  heicant  29626  opnmbllem0  29627  mblfinlem1  29628  mblfinlem2  29629  mblfinlem3  29630  mblfinlem4  29631  ismblfin  29632  volsupnfl  29636  itg2addnclem2  29644  itg2gt0cn  29647  ftc1anclem3  29669  ftc1anclem5  29671  ftc1anclem6  29672  ftc1anclem7  29673  ftc1anclem8  29674  ftc1anc  29675  comppfsc  29779  neibastop2lem  29781  tailfb  29798  indexdom  29828  cnresima  29863  istotbnd3  29870  sstotbnd2  29873  sstotbnd  29874  totbndbnd  29888  prdsbnd  29892  cntotbnd  29895  ismtyima  29902  heibor1lem  29908  heiborlem1  29910  heibor  29920  rrnval  29926  rrnequiv  29934  reheibor  29938  elrfirn  30231  cmpfiiin  30233  isnacs2  30242  isnacs3  30246  nacsfix  30248  coeq0i  30290  diophrw  30296  eldioph2lem2  30298  dnwech  30598  fnwe2lem2  30601  lmhmfgima  30634  pwssplit4  30639  hbt  30683  refsumcn  30983  cncmpmax  30985  climinf  31148  icccncfext  31226  dvsinax  31241  ditgeqiooicc  31278  itgsubsticclem  31293  fourierdlem12  31419  fourierdlem42  31449  fourierdlem54  31461  fourierdlem70  31477  fourierdlem76  31483  fourierdlem82  31489  fourierdlem85  31492  fourierdlem88  31495  fourierdlem93  31500  fourierdlem113  31520  fafvelrn  31722  lsatset  33787  lsatlss  33793  cdleme50rnlem  35340
  Copyright terms: Public domain W3C validator