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

Theorem ffn 5591
Description: A mapping is a function. (Contributed by NM, 2-Aug-1994.)
Assertion
Ref Expression
ffn  |-  ( F : A --> B  ->  F  Fn  A )

Proof of Theorem ffn
StepHypRef Expression
1 df-f 5458 . 2  |-  ( F : A --> B  <->  ( F  Fn  A  /\  ran  F  C_  B ) )
21simplbi 447 1  |-  ( F : A --> B  ->  F  Fn  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    C_ wss 3320   ran crn 4879    Fn wfn 5449   -->wf 5450
This theorem is referenced by:  ffun  5593  frel  5594  fdm  5595  fresin  5612  fresaun  5614  fresaunres2  5615  fcoi1  5617  feu  5619  fnconstg  5631  f1fn  5640  fofn  5655  dffo2  5657  f1ofn  5675  feqmptd  5779  fvco3  5800  suppss  5863  suppssr  5864  ffvelrn  5868  dff2  5881  dffo3  5884  dffo4  5885  dffo5  5886  f1ompt  5891  ffnfv  5894  fcompt  5904  fsn2  5908  fconst2g  5946  fconstfv  5954  fex  5969  dff13  6004  cocan1  6024  soisores  6047  off  6320  ofco  6324  caofref  6330  caofid0l  6332  caofid0r  6333  caofid1  6334  caofid2  6335  caofrss  6337  caoftrn  6339  suppssof1  6346  fo1stres  6370  fo2ndres  6371  1stcof  6374  2ndcof  6375  curry1f  6440  curry2f  6442  fparlem1  6446  fparlem2  6447  fo2ndf  6453  fnwelem  6461  fnse  6463  tposf2  6503  smo11  6626  smorndom  6630  mapsn  7055  omxpenlem  7209  pw2f1olem  7212  mapen  7271  mapxpen  7273  mapunen  7276  f1finf1o  7335  unirnffid  7398  fissuni  7411  fipreima  7412  indexfi  7414  intrnfi  7421  marypha2  7444  ordtypelem7  7493  oismo  7509  wemapso2lem  7519  wemapso  7520  wemapso2  7521  unxpwdom2  7556  ixpiunwdom  7559  cantnfle  7626  cantnflt  7627  cantnfp1lem2  7635  cantnfp1lem3  7636  cantnfp1  7637  oemapvali  7640  cantnflem1a  7641  cantnflem1c  7643  cantnflem3  7647  cantnflem4  7648  cantnf  7649  mapfien  7653  cnfcomlem  7656  cnfcom3  7661  tcrank  7808  fseqenlem1  7905  numacn  7930  infpwfien  7943  carduniima  7977  cardinfima  7978  dfacacn  8021  cfflb  8139  cofsmo  8149  cfcoflem  8152  coftr  8153  fin23lem40  8231  isf32lem2  8234  isf34lem7  8259  isf34lem6  8260  axdc3lem2  8331  ac6num  8359  ac6c4  8361  ac6s2  8366  ttukeylem6  8394  iunfo  8414  unirnfdomd  8442  pwcfsdom  8458  fpwwe2lem6  8510  fpwwe2lem8  8512  pwfseqlem3  8535  inar1  8650  tskcard  8656  tskuni  8658  tskurn  8664  gruima  8677  nqerrel  8809  recmulnq  8841  dmrecnq  8845  axpre-sup  9044  ofsubeq0  9997  ofnegsub  9998  ofsubge0  9999  dfz2  10299  uzn0  10501  rpnnen1lem3  10602  rpnnen1lem5  10604  unirnioo  11004  dfioo2  11005  ioorebas  11006  fseq1p1m1  11122  injresinjlem  11199  fsequb2  11315  fseqsupcl  11316  fseqsupubi  11317  seqf1olem2  11363  ser0f  11376  hashgval  11621  hashinf  11623  hashgval2  11652  iswrd  11729  wrdf  11733  wrdfin  11734  ccatlid  11748  ccatrid  11749  ccatass  11750  eqs1  11761  swrd0len  11769  swrdid  11772  ccatswrd  11773  swrdccat1  11774  swrdccat2  11775  cats1un  11790  revlen  11794  revccat  11798  revrev  11799  lenco  11801  s1co  11802  revco  11803  ccatco  11804  shftf  11894  uzin2  12148  rexanuz  12149  limsupgle  12271  limsuple  12272  limsupval2  12274  rlimres  12352  lo1res  12353  rlimresb  12359  o1of2  12406  o1rlimmul  12412  isercolllem2  12459  isercolllem3  12460  isercoll  12461  isercoll2  12462  climsup  12463  fsumss  12519  supcvg  12635  eff2  12700  reeff1  12721  tanval  12729  ruclem4  12833  ruclem11  12839  ruclem12  12840  eucalg  13078  prmreclem6  13289  1arithlem4  13294  1arith  13295  vdwmc  13346  vdwlem1  13349  vdwlem2  13350  vdwlem6  13354  vdwlem8  13356  vdwlem9  13357  vdwlem12  13360  vdwlem13  13361  ramval  13376  0ram  13388  0ram2  13389  0ramcl  13391  ramub1lem1  13394  ramcl  13397  firest  13660  pwsle  13714  pwsleval  13715  pwsvscaval  13717  mrcuni  13846  mrcun  13847  invf1o  13994  funcres2c  14098  isfull2  14108  arwhoma  14200  setcmon  14242  setcepi  14243  uncfcurf  14336  yoniso  14382  isacs4lem  14594  acsmapd  14604  prdsplusgcl  14726  prdsidlem  14727  prdsmndd  14728  resmhm2b  14761  mhmima  14763  mhmeql  14764  prdspjmhm  14766  pwsco1mhm  14769  pwsco2mhm  14770  gsumval2a  14782  gsumval2  14783  gsumwmhm  14790  frmdss2  14808  isgrpinv  14855  grpinvf1o  14861  prdsinvlem  14926  cycsubgcl  14966  ghmrn  15019  ghmpreima  15027  ghmeql  15028  ghmnsgima  15029  ghmnsgpreima  15030  ghmeqker  15032  ghmf1o  15035  gass  15078  cntzmhm  15137  efginvrel2  15359  efgsfo  15371  efgredleme  15375  efgredlem  15379  efgcpbllemb  15387  frgpup3lem  15409  0frgp  15411  ghmplusg  15461  gexex  15468  torsubg  15469  prdscmnd  15476  gsumval3a  15512  gsumval3eu  15513  gsumval3  15514  gsumzres  15517  gsumzaddlem  15526  gsumzsplit  15529  gsumzoppg  15539  gsumpt  15545  prdsgsum  15552  dprdfcntz  15573  dprdfadd  15578  dprdfeq0  15580  dprdf11  15581  dprdlub  15584  dprdspan  15585  dprdf1o  15590  dprd2dlem1  15599  dprd2db  15601  dmdprdpr  15607  dprdpr  15608  dpjlem  15609  ablfac1eu  15631  pgpfaclem1  15639  prdsmulrcl  15717  prdsrngd  15718  prdscrngd  15719  prds1  15720  isabvd  15908  srngf1o  15942  prdsvscacl  16044  prdslmodd  16045  lmhmco  16119  lmhmplusg  16120  lmhmvsca  16121  lmhmf1o  16122  lmhmima  16123  lmhmpreima  16124  lmhmrnlss  16126  lmhmeql  16131  lspextmo  16132  psrbaglesupp  16433  psrbagcon  16436  psrbaglefi  16437  psrbagconf1o  16439  gsumbagdiaglem  16440  psrvscaval  16456  psrlidm  16467  psrridm  16468  psrass1  16469  psrdi  16470  psrdir  16471  mplsubglem  16498  mplvscaval  16511  subrgmvrf  16525  mplmonmul  16527  mplbas2  16531  mvrf2  16552  mplind  16562  psrplusgpropd  16629  coe1add  16657  coe1addfv  16658  coe1sclmulfv  16675  cnfldplusf  16728  cnfldsub  16729  chrrhm  16812  znunit  16844  pjfo  16942  lecldbas  17283  lmbr2  17323  cncnpi  17342  cncnp  17344  cnrest2  17350  cnpdis  17357  lmss  17362  lmff  17365  lmcnp  17368  pnrmopn  17407  cnt0  17410  cnt1  17414  cnhaus  17418  dnsconst  17442  rncmp  17459  cmpsub  17463  tgcmp  17464  hauscmplem  17469  bwth  17473  concn  17489  2ndcctbss  17518  2ndcomap  17521  2ndcsep  17522  1stccnp  17525  kgenidm  17579  iskgen2  17580  1stckgenlem  17585  1stckgen  17586  kgen2cn  17591  ptpjpre1  17603  ptbasfi  17613  pttop  17614  ptopn  17615  ptuni  17626  ptval2  17633  tx1cn  17641  tx2cn  17642  ptpjcn  17643  ptpjopn  17644  ptclsg  17647  ptcnplem  17653  ptcnp  17654  upxp  17655  txcnmpt  17656  uptx  17657  txtube  17672  txcmplem1  17673  txcmplem2  17674  hauseqlcld  17678  txkgen  17684  xkohaus  17685  xkoptsub  17686  xkopt  17687  xkococnlem  17691  xkococn  17692  cnmpt11  17695  cnmpt21  17703  cnmpt22f  17707  cnmptcom  17710  qtopss  17747  qtopeu  17748  qtopomap  17750  qtopcmap  17751  kqffn  17757  hmeof1o2  17795  ptcmpfi  17845  xkocnv  17846  zfbas  17928  uzrest  17929  rnelfmlem  17984  rnelfm  17985  fmfnfmlem2  17987  fmfnfm  17990  lmflf  18037  alexsubALT  18082  ptcmplem1  18083  cnextfres  18099  tmdgsum  18125  clssubg  18138  ghmcnp  18144  tgphaus  18146  divstgplem  18150  prdstmdd  18153  prdstgpd  18154  tsmsres  18173  tsmsxplem1  18182  ucncn  18315  fmucnd  18322  psmetxrge0  18344  isxmet2d  18357  xmettpos  18379  prdsmet  18400  imasdsf1olem  18403  blrnps  18438  blrn  18439  blelrnps  18446  blelrn  18447  xmeterval  18462  xmetresbl  18467  tmslem  18512  tmsxms  18516  imasf1oxms  18519  comet  18543  stdbdxmet  18545  met2ndci  18552  prdsxmslem2  18559  prdsxms  18560  blval2  18605  metuel2  18609  isngp2  18644  isngp3  18645  tngngp2  18693  isnghm  18757  nmotri  18773  qtopbaslem  18792  qdensere  18804  cnbl0  18808  cnblcld  18809  cnfldms  18810  blssioo  18826  tgioo  18827  tgqioo  18831  xrtgioo  18837  xrsdsre  18841  xrge0tsms  18865  metdsre  18883  iimulcn  18963  bndth  18983  evth  18984  lebnumlem3  18988  nmhmcn  19128  cphsqrcl  19147  lmmbr2  19212  fmcfil  19225  caucfil  19236  causs  19251  lmcau  19265  bcthlem4  19280  bcth3  19284  cncms  19309  cnfldcusp  19311  ivthicc  19355  evthicc2  19357  ovolfioo  19364  ovolficc  19365  ovolficcss  19366  ovolfsf  19368  ovolmge0  19373  ovollb2lem  19384  ovolunlem1a  19392  ovoliunlem1  19398  ovoliunlem2  19399  ovoliun  19401  ovoliun2  19402  ovolshftlem1  19405  ovolscalem1  19409  ovolicc1  19412  ovolicc2lem4  19416  ovolicc2  19418  ismbl  19422  voliunlem1  19444  voliunlem2  19445  voliunlem3  19446  volsup  19450  ioombl1lem2  19453  ioombl1lem4  19455  ioorf  19465  ioorinv  19468  ioorcl  19469  uniiccdif  19470  uniioovol  19471  uniiccvol  19472  uniioombllem2  19475  uniioombllem3  19477  uniioombllem4  19478  uniioombllem6  19480  dyaddisj  19488  dyadmax  19490  dyadmbllem  19491  dyadmbl  19492  opnmbllem  19493  opnmblALT  19495  volsup2  19497  vitalilem4  19503  mbfdm  19520  mbfima  19524  mbfid  19528  ismbfd  19532  mbfeqalem  19534  mbfres2  19537  mbfmulc2lem  19539  mbfmax  19541  mbfposr  19544  mbfimaopnlem  19547  mbfaddlem  19552  mbfadd  19553  mbfsub  19554  mbfsup  19556  mbfinf  19557  mbflimsup  19558  0plef  19564  itg1val2  19576  itg1ge0  19578  i1f1lem  19581  itg11  19583  itg1addlem1  19584  i1faddlem  19585  i1fmullem  19586  i1fadd  19587  i1fmul  19588  itg1addlem4  19591  i1fmulclem  19594  i1fmulc  19595  itg1mulc  19596  i1fres  19597  i1fpos  19598  itg10a  19602  itg1ge0a  19603  itg1lea  19604  itg1le  19605  itg1climres  19606  mbfi1fseqlem3  19609  mbfi1fseqlem4  19610  mbfi1fseqlem5  19611  mbfi1flimlem  19614  mbfmullem2  19616  mbfmul  19618  xrge0f  19623  itg2ge0  19627  itg20  19629  itg2seq  19634  itg2lea  19636  itg2splitlem  19640  itg2split  19641  itg2monolem1  19642  itg2monolem2  19643  itg2monolem3  19644  itg2mono  19645  itg2i1fseqle  19646  itg2i1fseq  19647  itg2i1fseq2  19648  itg2addlem  19650  itg2gt0  19652  itg2cnlem1  19653  itg2cnlem2  19654  itg2cn  19655  itgitg1  19700  bddmulibl  19730  bddibl  19731  limciun  19781  dvres  19798  dvres3a  19801  dvidlem  19802  cpnres  19823  dvaddbr  19824  dvmulbr  19825  dvaddf  19828  dvcmulf  19831  dvfre  19837  dvrec  19841  dvmptres3  19842  dvcnvlem  19860  rolle  19874  dvlip2  19879  dveq0  19884  dv11cn  19885  dvgt0lem2  19887  dvivthlem2  19893  dvivth  19894  dvne0  19895  lhop1lem  19897  lhop1  19898  lhop2  19899  lhop  19900  ftc1cn  19927  evlslem3  19935  evlslem1  19936  evlseu  19937  evlsvar  19944  evl1addd  19954  evl1subd  19955  evl1muld  19956  mpfconst  19959  mpfproj  19960  mpfsubrg  19961  mpfind  19965  pf1const  19966  pf1id  19967  pf1subrg  19968  mpfpf1  19971  pf1mpf  19972  pf1ind  19975  tdeglem4  19983  mdegleb  19987  mdegldg  19989  mdegaddle  19997  deg1fvi  20008  uc1pmon1p  20074  ply1remlem  20085  ply1rem  20086  fta1glem1  20088  fta1glem2  20089  fta1g  20090  fta1blem  20091  ig1peu  20094  ig1pdvds  20099  plyco0  20111  plyeq0lem  20129  plyeq0  20130  plypf1  20131  plyaddlem1  20132  coeeulem  20143  dgrlem  20148  dgrub  20153  dgrlb  20155  coeaddlem  20167  coemulc  20173  dgradd2  20186  dgrcolem2  20192  ofmulrt  20199  plyreres  20200  plydivlem3  20212  plydivlem4  20213  plydiveu  20215  plyremlem  20221  plyrem  20222  fta1lem  20224  fta1  20225  vieta1lem1  20227  vieta1lem2  20228  vieta1  20229  plyexmo  20230  elaa  20233  elqaalem3  20238  aannenlem1  20245  aalioulem2  20250  ulmuni  20308  ulmdvlem1  20316  ulmdv  20319  mbfulm  20322  iblulm  20323  itgulm  20324  pserulm  20338  psercnlem2  20340  psercnlem1  20341  psercn  20342  abelth  20357  reeff1o  20363  pilem1  20367  recosf1o  20437  resinf1o  20438  efif1olem3  20446  efif1olem4  20447  efifo  20449  eff1olem  20450  ellogrn  20457  logcn  20538  dvloglem  20539  logf1o2  20541  efopnlem1  20547  efopnlem2  20548  efopn  20549  logtayl  20551  cxpcn3lem  20631  cxpcn3  20632  resqrcn  20633  asinneg  20726  areambl  20797  rlimcnp2  20805  jensen  20827  amgm  20829  emcllem7  20840  basellem3  20865  basellem4  20866  basellem7  20869  basellem9  20871  sqff1o  20965  dvdsmulf1o  20979  fsumdvdsmul  20980  dchrelbas2  21021  dchrmulcl  21033  dchrfi  21039  dchreq  21042  dchrresb  21043  dchrinv  21045  dchr1re  21047  sumdchr2  21054  dchr2sum  21057  lgsqrlem2  21126  lgsqrlem3  21127  rpvmasum2  21206  dchrisum0re  21207  ostthlem1  21321  ostth  21333  nbgraf1olem5  21455  is2wlk  21565  redwlklem  21605  fargshiftfv  21622  fargshiftf  21623  fargshiftf1  21624  fargshiftfo  21625  constr3pthlem3  21644  vdgr0  21671  eupacl  21691  eupapf  21694  eupaseg  21695  eupares  21697  eupath  21703  vdegp1ai  21706  vdegp1bi  21707  isgrpo2  21785  issubgoi  21898  ginvsn  21937  efghgrp  21961  vcoprnelem  22057  nvinvfval  22121  cnnvm  22174  sspg  22227  ssps  22229  sspmlem  22231  sspn  22235  nvo00  22262  nmlno0lem  22294  lnon0  22299  phoeqi  22359  ubthlem1  22372  hhip  22679  hhssabloi  22762  hhssnv  22764  hhsssh  22769  occllem  22805  shsel  22816  chscllem2  23140  pjfn  23211  df0op2  23255  hoeq  23263  hocofni  23270  hoaddfni  23273  hosubfni  23274  hon0  23296  ho01i  23331  hoeq1  23333  elnlfn  23431  kbpj  23459  nmlnop0iALT  23498  lnopco0i  23507  imaelshi  23561  nlelchi  23564  rnbra  23610  cnvbraval  23613  kbass2  23620  kbass5  23623  hmopidmchi  23654  hmopidmpji  23655  elpjrn  23693  ofrn2  24053  off2  24054  ofresid  24055  xppreima2  24060  feqmptdf  24075  fcomptf  24077  ofpreima  24081  hashresfn  24156  xrge0tsmsd  24223  kerunit  24261  kerf1hrm  24262  hauseqcn  24293  xpinpreima  24304  xpinpreima2  24305  tpr2rico  24310  mndpluscn  24312  rmulccn  24314  raddcn  24315  xrge0pluscn  24326  xrge0tmdOLD  24331  rge0scvg  24335  elzrhunit  24363  qqhval2lem  24365  qqhf  24370  qqhre  24386  indpi1  24419  indpreima  24422  esumcvg  24476  ofcf  24486  measfn  24558  meascnbl  24573  1stmbfm  24610  2ndmbfm  24611  mbfmcnt  24618  sibfof  24654  sitgclcn  24658  rrvfn  24703  lgamgulm2  24820  txsconlem  24927  iccllyscon  24937  rellyscon  24938  cvmseu  24963  cvmopnlem  24965  cvmliftmolem1  24968  cvmliftmolem2  24969  cvmliftlem6  24977  cvmliftlem7  24978  cvmliftlem8  24979  cvmliftlem9  24980  cvmliftlem10  24981  cvmliftlem11  24982  cvmliftlem15  24985  cvmlift2lem9a  24990  cvmlift2lem6  24995  cvmlift2lem7  24996  cvmlift2lem10  24999  cvmlift2lem12  25001  cvmliftphtlem  25004  cvmlift3lem8  25013  cvmlift3lem9  25014  ghomgrpilem2  25097  ghomfo  25102  prodf1f  25220  iprodefisumlem  25317  fprb  25397  soseq  25529  fullfunfnv  25791  fullfunfv  25792  eqeefv  25842  axlowdimlem6  25886  axlowdimlem8  25888  axlowdimlem9  25889  axlowdimlem11  25891  axlowdimlem12  25892  axlowdimlem14  25894  axlowdimlem17  25897  opnmbllem0  26242  mblfinlem1  26243  mblfinlem2  26244  volsupnfl  26251  cnambfre  26255  itg2addnclem  26256  itg2addnclem2  26257  itg2addnclem3  26258  itg2addnc  26259  itg2gt0cn  26260  ftc1cnnc  26279  ftc1anclem3  26282  ftc1anclem5  26284  ftc1anclem7  26286  ftc1anclem8  26287  ftc1anc  26288  areacirc  26297  comppfsc  26387  tailfb  26406  filnetlem4  26410  indexdom  26436  sdclem2  26446  istotbnd3  26480  sstotbnd2  26483  sstotbnd  26484  isbndx  26491  isbnd3  26493  isbnd3b  26494  prdsbnd  26502  prdstotbnd  26503  ismtyhmeolem  26513  heibor1lem  26518  heiborlem1  26520  heibor  26530  rrnmet  26538  rrnequiv  26544  grpokerinj  26560  isdrngo2  26574  keridl  26642  ralxpmap  26742  lcomfsup  26747  elrfirn  26749  ismrcd1  26752  ismrcd2  26753  istopclsd  26754  isnacs2  26760  isnacs3  26764  nacsfix  26766  mapfzcons1  26773  mzpaddmpt  26798  mzpmulmpt  26799  mzpsubst  26805  mzpcompact2lem  26808  eq0rabdioph  26835  eldioph4b  26872  diophren  26874  mzpcong  27037  pw2f1ocnv  27108  pw2f1o2val2  27111  fnwe2lem2  27126  islmodfg  27144  kercvrlsm  27158  lmhmfgsplit  27161  pwssplit1  27165  pwssplit4  27168  dsmmbas2  27180  dsmm0cl  27183  dsmmacl  27184  dsmmsubg  27186  dsmmlss  27187  frlmbas  27200  frlmvscaval  27208  frlmsslss2  27222  frlmssuvc2  27224  frlmsslsp  27225  frlmlbs  27226  frlmup1  27227  frlmup2  27228  frlmup3  27229  frlmup4  27230  ellspd  27231  lindfmm  27274  lsslindf  27277  islindf4  27285  hbt  27311  dgrsub2  27316  mpaaeu  27332  rngunsnply  27355  f1omvdconj  27366  pmtrmvd  27375  pmtrfinv  27379  symgtrinv  27390  mamulid  27435  mamurid  27436  mamuass  27437  mamudi  27438  mamudir  27439  mamuvs1  27440  mamuvs2  27441  mendrng  27477  idomrootle  27488  proot1mul  27492  proot1hash  27496  proot1ex  27497  deg1mhm  27503  fgraphopab  27506  hausgraph  27508  caofcan  27517  ofsubid  27518  ofmul12  27519  ofdivrec  27520  ofdivcan4  27521  ofdivdiv2  27522  expgrowthi  27527  dvconstbi  27528  expgrowth  27529  rfcnpre1  27666  rfcnpre2  27678  cncmpmax  27679  rfcnpre3  27680  rfcnpre4  27681  refsum2cnlem1  27684  climinf  27708  dvcosre  27717  stoweidlem48  27773  fafvelrn  28010  ffnafv  28011  f0bi  28075  imarnf1pr  28084  2ffzeq  28121  2ffzoeq  28140  hashfirdm  28165  hashfzdm  28166  wrdfn  28171  cshword  28235  frgrancvvdeqlemB  28427  lfl1  29868  lfladdcl  29869  lflvscl  29875  ellkr  29887  lkr0f  29892  lkrsc  29895  eqlkr2  29898  eqlkr3  29899  ldualvaddval  29929  ldualvsval  29936  cdleme50rnlem  31341  tendoeq1  31561
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 5458
  Copyright terms: Public domain W3C validator