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

Theorem ffn 5389
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 5259 . 2  |-  ( F : A --> B  <->  ( F  Fn  A  /\  ran  F  C_  B ) )
21simplbi 446 1  |-  ( F : A --> B  ->  F  Fn  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    C_ wss 3152   ran crn 4690    Fn wfn 5250   -->wf 5251
This theorem is referenced by:  ffun  5391  frel  5392  fdm  5393  fresin  5410  fresaun  5412  fresaunres2  5413  fcoi1  5415  feu  5417  fnconstg  5429  f1fn  5438  fofn  5453  dffo2  5455  f1ofn  5473  feqmptd  5575  fvco3  5596  suppss  5658  suppssr  5659  ffvelrn  5663  dff2  5672  dffo3  5675  dffo4  5676  dffo5  5677  f1ompt  5682  ffnfv  5685  fcompt  5694  fsn2  5698  fconst2g  5728  fconstfv  5734  fex  5749  dff13  5783  cocan1  5801  soisores  5824  off  6093  ofco  6097  caofref  6103  caofid0l  6105  caofid0r  6106  caofid1  6107  caofid2  6108  caofrss  6110  caoftrn  6112  suppssof1  6119  fo1stres  6143  fo2ndres  6144  1stcof  6147  2ndcof  6148  curry1f  6212  curry2f  6214  fparlem1  6218  fparlem2  6219  fnwelem  6230  fnse  6232  tposf2  6258  smo11  6381  smorndom  6385  mapsn  6809  omxpenlem  6963  pw2f1olem  6966  mapen  7025  mapxpen  7027  mapunen  7030  f1finf1o  7086  unirnffid  7147  fissuni  7160  fipreima  7161  indexfi  7163  intrnfi  7170  marypha2  7192  ordtypelem7  7239  oismo  7255  wemapso2lem  7265  wemapso  7266  wemapso2  7267  unxpwdom2  7302  ixpiunwdom  7305  cantnfle  7372  cantnflt  7373  cantnfp1lem2  7381  cantnfp1lem3  7382  cantnfp1  7383  oemapvali  7386  cantnflem1a  7387  cantnflem1c  7389  cantnflem3  7393  cantnflem4  7394  cantnf  7395  mapfien  7399  cnfcomlem  7402  cnfcom3  7407  tcrank  7554  fseqenlem1  7651  numacn  7676  infpwfien  7689  carduniima  7723  cardinfima  7724  dfacacn  7767  cfflb  7885  cofsmo  7895  cfcoflem  7898  coftr  7899  fin23lem40  7977  isf32lem2  7980  isf34lem7  8005  isf34lem6  8006  axdc3lem2  8077  ac6num  8106  ac6c4  8108  ac6s2  8113  ttukeylem6  8141  iunfo  8161  unirnfdomd  8189  pwcfsdom  8205  fpwwe2lem6  8257  fpwwe2lem8  8259  pwfseqlem3  8282  inar1  8397  tskcard  8403  tskuni  8405  tskurn  8411  gruima  8424  nqerrel  8556  recmulnq  8588  dmrecnq  8592  axpre-sup  8791  ofsubeq0  9743  ofnegsub  9744  ofsubge0  9745  dfz2  10041  uzn0  10243  rpnnen1lem3  10344  rpnnen1lem5  10346  unirnioo  10743  dfioo2  10744  ioorebas  10745  fseq1p1m1  10857  fsequb2  11038  fseqsupcl  11039  fseqsupubi  11040  seqf1olem2  11086  ser0f  11099  hashgval  11340  hashinf  11342  hashgval2  11360  iswrd  11415  wrdf  11419  wrdfin  11420  ccatlid  11434  ccatrid  11435  ccatass  11436  eqs1  11447  swrd0len  11455  swrdid  11458  ccatswrd  11459  swrdccat1  11460  swrdccat2  11461  cats1un  11476  revlen  11480  revccat  11484  revrev  11485  lenco  11487  s1co  11488  revco  11489  ccatco  11490  shftf  11574  uzin2  11828  rexanuz  11829  limsupgle  11951  limsuple  11952  limsupval2  11954  rlimres  12032  lo1res  12033  rlimresb  12039  o1of2  12086  o1rlimmul  12092  isercolllem2  12139  isercolllem3  12140  isercoll  12141  isercoll2  12142  climsup  12143  fsumss  12198  supcvg  12314  eff2  12379  reeff1  12400  tanval  12408  ruclem4  12512  ruclem11  12518  ruclem12  12519  eucalg  12757  prmreclem6  12968  1arithlem4  12973  1arith  12974  vdwmc  13025  vdwlem1  13028  vdwlem2  13029  vdwlem6  13033  vdwlem8  13035  vdwlem9  13036  vdwlem12  13039  vdwlem13  13040  ramval  13055  0ram  13067  0ram2  13068  0ramcl  13070  ramub1lem1  13073  ramcl  13076  firest  13337  pwsle  13391  pwsleval  13392  pwsvscaval  13394  mrcuni  13523  mrcun  13524  invf1o  13671  funcres2c  13775  isfull2  13785  arwhoma  13877  setcmon  13919  setcepi  13920  uncfcurf  14013  yoniso  14059  isacs4lem  14271  acsmapd  14281  prdsplusgcl  14403  prdsidlem  14404  prdsmndd  14405  resmhm2b  14438  mhmima  14440  mhmeql  14441  prdspjmhm  14443  pwsco1mhm  14446  pwsco2mhm  14447  gsumval2a  14459  gsumval2  14460  gsumwmhm  14467  frmdss2  14485  isgrpinv  14532  grpinvf1o  14538  prdsinvlem  14603  cycsubgcl  14643  ghmrn  14696  ghmpreima  14704  ghmeql  14705  ghmnsgima  14706  ghmnsgpreima  14707  ghmeqker  14709  ghmf1o  14712  gass  14755  cntzmhm  14814  efginvrel2  15036  efgsfo  15048  efgredleme  15052  efgredlem  15056  efgcpbllemb  15064  frgpup3lem  15086  0frgp  15088  ghmplusg  15138  gexex  15145  torsubg  15146  prdscmnd  15153  gsumval3a  15189  gsumval3eu  15190  gsumval3  15191  gsumzres  15194  gsumzaddlem  15203  gsumzsplit  15206  gsumzoppg  15216  gsumpt  15222  prdsgsum  15229  dprdfcntz  15250  dprdfadd  15255  dprdfeq0  15257  dprdf11  15258  dprdlub  15261  dprdspan  15262  dprdf1o  15267  dprd2dlem1  15276  dprd2db  15278  dmdprdpr  15284  dprdpr  15285  dpjlem  15286  ablfac1eu  15308  pgpfaclem1  15316  prdsmulrcl  15394  prdsrngd  15395  prdscrngd  15396  prds1  15397  isabvd  15585  srngf1o  15619  prdsvscacl  15725  prdslmodd  15726  lmhmco  15800  lmhmplusg  15801  lmhmvsca  15802  lmhmf1o  15803  lmhmima  15804  lmhmpreima  15805  lmhmrnlss  15807  lmhmeql  15812  lspextmo  15813  psrbaglesupp  16114  psrbagcon  16117  psrbaglefi  16118  psrbagconf1o  16120  gsumbagdiaglem  16121  psrvscaval  16137  psrlidm  16148  psrridm  16149  psrass1  16150  psrdi  16151  psrdir  16152  mplsubglem  16179  mplvscaval  16192  subrgmvrf  16206  mplmonmul  16208  mplbas2  16212  mvrf2  16233  mplind  16243  psrplusgpropd  16313  coe1add  16341  coe1addfv  16342  coe1sclmulfv  16359  cnfldplusf  16401  cnfldsub  16402  chrrhm  16485  znunit  16517  pjfo  16615  lecldbas  16949  lmbr2  16989  cncnpi  17007  cncnp  17009  cnrest2  17014  cnpdis  17021  lmss  17026  lmff  17029  lmcnp  17032  pnrmopn  17071  cnt0  17074  cnt1  17078  cnhaus  17082  dnsconst  17106  rncmp  17123  cmpsub  17127  tgcmp  17128  hauscmplem  17133  concn  17152  2ndcctbss  17181  2ndcomap  17184  2ndcsep  17185  1stccnp  17188  kgenidm  17242  iskgen2  17243  1stckgenlem  17248  1stckgen  17249  kgen2cn  17254  ptpjpre1  17266  ptbasfi  17276  pttop  17277  ptopn  17278  ptuni  17289  ptval2  17296  tx1cn  17303  tx2cn  17304  ptpjcn  17305  ptpjopn  17306  ptclsg  17309  ptcnplem  17315  ptcnp  17316  upxp  17317  txcnmpt  17318  uptx  17319  txtube  17334  txcmplem1  17335  txcmplem2  17336  hauseqlcld  17340  txkgen  17346  xkohaus  17347  xkoptsub  17348  xkopt  17349  xkococnlem  17353  xkococn  17354  cnmpt11  17357  cnmpt21  17365  cnmpt22f  17369  cnmptcom  17372  qtopss  17406  qtopeu  17407  qtopomap  17409  qtopcmap  17410  kqffn  17416  hmeof1o2  17454  ptcmpfi  17504  xkocnv  17505  zfbas  17591  uzrest  17592  rnelfmlem  17647  rnelfm  17648  fmfnfmlem2  17650  fmfnfm  17653  lmflf  17700  alexsubALT  17745  ptcmplem1  17746  tmdgsum  17778  clssubg  17791  ghmcnp  17797  tgphaus  17799  divstgplem  17803  prdstmdd  17806  prdstgpd  17807  tsmsres  17826  tsmsxplem1  17835  isxmet2d  17892  xmettpos  17913  prdsmet  17934  imasdsf1olem  17937  blrn  17962  blelrn  17967  xmeterval  17978  xmetresbl  17983  tmslem  18028  tmsxms  18032  imasf1oxms  18035  comet  18059  stdbdxmet  18061  met2ndci  18068  prdsxmslem2  18075  prdsxms  18076  isngp2  18119  isngp3  18120  tngngp2  18168  isnghm  18232  nmotri  18248  qtopbaslem  18267  qdensere  18279  cnbl0  18283  cnblcld  18284  cnfldms  18285  blssioo  18301  tgioo  18302  tgqioo  18306  xrtgioo  18312  xrsdsre  18316  xrge0tsms  18339  metdsre  18357  iimulcn  18436  bndth  18456  evth  18457  lebnumlem3  18461  nmhmcn  18601  cphsqrcl  18620  lmmbr2  18685  fmcfil  18698  caucfil  18709  causs  18724  lmcau  18738  bcthlem4  18749  bcth3  18753  cncms  18774  ivthicc  18818  evthicc2  18820  ovolfioo  18827  ovolficc  18828  ovolficcss  18829  ovolfsf  18831  ovolmge0  18836  ovollb2lem  18847  ovolunlem1a  18855  ovoliunlem1  18861  ovoliunlem2  18862  ovoliun  18864  ovoliun2  18865  ovolshftlem1  18868  ovolscalem1  18872  ovolicc1  18875  ovolicc2lem4  18879  ovolicc2  18881  ismbl  18885  voliunlem1  18907  voliunlem2  18908  voliunlem3  18909  volsup  18913  ioombl1lem2  18916  ioombl1lem4  18918  ioorf  18928  ioorinv  18931  ioorcl  18932  uniiccdif  18933  uniioovol  18934  uniiccvol  18935  uniioombllem2  18938  uniioombllem3  18940  uniioombllem4  18941  uniioombllem6  18943  dyaddisj  18951  dyadmax  18953  dyadmbllem  18954  dyadmbl  18955  opnmbllem  18956  opnmblALT  18958  volsup2  18960  vitalilem4  18966  mbfdm  18983  mbfima  18987  mbfid  18991  ismbfd  18995  mbfeqalem  18997  mbfres2  19000  mbfmulc2lem  19002  mbfmax  19004  mbfposr  19007  mbfimaopnlem  19010  mbfaddlem  19015  mbfadd  19016  mbfsub  19017  mbfsup  19019  mbfinf  19020  mbflimsup  19021  0plef  19027  itg1val2  19039  itg1ge0  19041  i1f1lem  19044  itg11  19046  itg1addlem1  19047  i1faddlem  19048  i1fmullem  19049  i1fadd  19050  i1fmul  19051  itg1addlem4  19054  i1fmulclem  19057  i1fmulc  19058  itg1mulc  19059  i1fres  19060  i1fpos  19061  itg10a  19065  itg1ge0a  19066  itg1lea  19067  itg1le  19068  itg1climres  19069  mbfi1fseqlem3  19072  mbfi1fseqlem4  19073  mbfi1fseqlem5  19074  mbfi1flimlem  19077  mbfmullem2  19079  mbfmul  19081  xrge0f  19086  itg2ge0  19090  itg20  19092  itg2seq  19097  itg2lea  19099  itg2splitlem  19103  itg2split  19104  itg2monolem1  19105  itg2monolem2  19106  itg2monolem3  19107  itg2mono  19108  itg2i1fseqle  19109  itg2i1fseq  19110  itg2i1fseq2  19111  itg2addlem  19113  itg2gt0  19115  itg2cnlem1  19116  itg2cnlem2  19117  itg2cn  19118  itgitg1  19163  bddmulibl  19193  bddibl  19194  limciun  19244  dvres  19261  dvres3a  19264  dvidlem  19265  cpnres  19286  dvaddbr  19287  dvmulbr  19288  dvaddf  19291  dvcmulf  19294  dvfre  19300  dvrec  19304  dvmptres3  19305  dvcnvlem  19323  rolle  19337  dvlip2  19342  dveq0  19347  dv11cn  19348  dvgt0lem2  19350  dvivthlem2  19356  dvivth  19357  dvne0  19358  lhop1lem  19360  lhop1  19361  lhop2  19362  lhop  19363  ftc1cn  19390  evlslem3  19398  evlslem1  19399  evlseu  19400  evlsvar  19407  evl1addd  19417  evl1subd  19418  evl1muld  19419  mpfconst  19422  mpfproj  19423  mpfsubrg  19424  mpfind  19428  pf1const  19429  pf1id  19430  pf1subrg  19431  mpfpf1  19434  pf1mpf  19435  pf1ind  19438  tdeglem4  19446  mdegleb  19450  mdegldg  19452  mdegaddle  19460  deg1fvi  19471  uc1pmon1p  19537  ply1remlem  19548  ply1rem  19549  fta1glem1  19551  fta1glem2  19552  fta1g  19553  fta1blem  19554  ig1peu  19557  ig1pdvds  19562  plyco0  19574  plyeq0lem  19592  plyeq0  19593  plypf1  19594  plyaddlem1  19595  coeeulem  19606  dgrlem  19611  dgrub  19616  dgrlb  19618  coeaddlem  19630  coemulc  19636  dgradd2  19649  dgrcolem2  19655  ofmulrt  19662  plyreres  19663  plydivlem3  19675  plydivlem4  19676  plydiveu  19678  plyremlem  19684  plyrem  19685  fta1lem  19687  fta1  19688  vieta1lem1  19690  vieta1lem2  19691  vieta1  19692  plyexmo  19693  elaa  19696  elqaalem3  19701  aannenlem1  19708  aalioulem2  19713  ulmdvlem1  19777  ulmdv  19780  mbfulm  19782  iblulm  19783  itgulm  19784  pserulm  19798  psercnlem2  19800  psercnlem1  19801  psercn  19802  abelth  19817  reeff1o  19823  pilem1  19827  recosf1o  19897  resinf1o  19898  efif1olem3  19906  efif1olem4  19907  efifo  19909  eff1olem  19910  ellogrn  19917  logcn  19994  dvloglem  19995  logf1o2  19997  efopnlem1  20003  efopnlem2  20004  efopn  20005  logtayl  20007  cxpcn3lem  20087  cxpcn3  20088  resqrcn  20089  asinneg  20182  areambl  20253  rlimcnp2  20261  jensen  20283  amgm  20285  emcllem7  20295  basellem3  20320  basellem4  20321  basellem7  20324  basellem9  20326  sqff1o  20420  dvdsmulf1o  20434  fsumdvdsmul  20435  dchrelbas2  20476  dchrmulcl  20488  dchrfi  20494  dchreq  20497  dchrresb  20498  dchrinv  20500  dchr1re  20502  sumdchr2  20509  dchr2sum  20512  lgsqrlem2  20581  lgsqrlem3  20582  rpvmasum2  20661  dchrisum0re  20662  ostthlem1  20776  ostth  20788  isgrpo2  20864  issubgoi  20977  ginvsn  21016  efghgrp  21040  vcoprnelem  21134  nvinvfval  21198  cnnvm  21251  sspg  21304  ssps  21306  sspmlem  21308  sspn  21312  nvo00  21339  nmlno0lem  21371  lnon0  21376  phoeqi  21436  ubthlem1  21449  hhip  21756  hhssabloi  21839  hhssnv  21841  hhsssh  21846  occllem  21882  shsel  21893  chscllem2  22217  pjfn  22288  df0op2  22332  hoeq  22340  hocofni  22347  hoaddfni  22350  hosubfni  22351  hon0  22373  ho01i  22408  hoeq1  22410  elnlfn  22508  kbpj  22536  nmlnop0iALT  22575  lnopco0i  22584  imaelshi  22638  nlelchi  22641  rnbra  22687  cnvbraval  22690  kbass2  22697  kbass5  22700  hmopidmchi  22731  hmopidmpji  22732  elpjrn  22770  hashresfn  23173  ofrn2  23207  off2  23208  xppreima2  23212  feqmptdf  23228  fcomptf  23230  xpinpreima  23290  xpinpreima2  23291  tpr2rico  23296  mndpluscn  23299  rmulccn  23301  raddcn  23302  xrge0pluscn  23322  xrge0tmdALT  23327  rge0scvg  23373  xrge0tsmsd  23382  esumcvg  23454  ofcf  23464  measfn  23534  meascnbl  23546  1stmbfm  23565  2ndmbfm  23566  mbfmcnt  23573  indpi1  23605  indpreima  23608  rrvfn  23648  coinflipspace  23681  txsconlem  23771  iccllyscon  23781  rellyscon  23782  cvmseu  23807  cvmopnlem  23809  cvmliftmolem1  23812  cvmliftmolem2  23813  cvmliftlem6  23821  cvmliftlem7  23822  cvmliftlem8  23823  cvmliftlem9  23824  cvmliftlem10  23825  cvmliftlem11  23826  cvmliftlem15  23829  cvmlift2lem9a  23834  cvmlift2lem6  23839  cvmlift2lem7  23840  cvmlift2lem10  23843  cvmlift2lem12  23845  cvmliftphtlem  23848  cvmlift3lem8  23857  cvmlift3lem9  23858  eupacl  23884  eupapf  23887  eupaseg  23888  vdgr0  23892  eupares  23899  eupath  23905  vdegp1ai  23908  vdegp1bi  23909  ghomgrpilem2  23993  ghomfo  23998  fprb  24129  soseq  24254  fullfunfnv  24484  fullfunfv  24485  eqeefv  24531  axlowdimlem6  24575  axlowdimlem8  24577  axlowdimlem9  24578  axlowdimlem11  24580  axlowdimlem12  24581  axlowdimlem14  24583  axlowdimlem17  24586  areacirc  24931  surjsec2  25120  injsurinj  25149  npincppr  25159  gapm2  25369  curgrpact  25372  grpodivfo  25374  bsi  25501  intopcoaconb  25540  intopcoaconc  25541  bwt2  25592  intrn  25599  altretop  25600  bsi2  25639  bsi3  25641  bsi4  25643  fnctartar  25907  fnctartar2  25908  clscnc  26010  comppfsc  26307  tailfb  26326  filnetlem4  26330  indexdom  26413  sdclem2  26452  istotbnd3  26495  sstotbnd2  26498  sstotbnd  26499  isbndx  26506  isbnd3  26508  isbnd3b  26509  prdsbnd  26517  prdstotbnd  26518  ismtyhmeolem  26528  heibor1lem  26533  heiborlem1  26535  heibor  26545  rrnmet  26553  rrnequiv  26559  grpokerinj  26575  isdrngo2  26589  keridl  26657  ralxpmap  26761  lcomfsup  26768  elrfirn  26770  ismrcd1  26773  ismrcd2  26774  istopclsd  26775  isnacs2  26781  isnacs3  26785  nacsfix  26787  mapfzcons1  26794  mzpaddmpt  26819  mzpmulmpt  26820  mzpsubst  26826  mzpcompact2lem  26829  eq0rabdioph  26856  eldioph4b  26894  diophren  26896  mzpcong  27059  pw2f1ocnv  27130  pw2f1o2val2  27133  fnwe2lem2  27148  islmodfg  27167  kercvrlsm  27181  lmhmfgsplit  27184  pwssplit1  27188  pwssplit4  27191  dsmmbas2  27203  dsmm0cl  27206  dsmmacl  27207  dsmmsubg  27209  dsmmlss  27210  frlmbas  27223  frlmvscaval  27231  frlmsslss2  27245  frlmssuvc2  27247  frlmsslsp  27248  frlmlbs  27249  frlmup1  27250  frlmup2  27251  frlmup3  27252  frlmup4  27253  ellspd  27254  lindfmm  27297  lsslindf  27300  islindf4  27308  hbt  27334  dgrsub2  27339  mpaaeu  27355  rngunsnply  27378  f1omvdconj  27389  pmtrmvd  27398  pmtrfinv  27402  symgtrinv  27413  mamulid  27458  mamurid  27459  mamuass  27460  mamudi  27461  mamudir  27462  mamuvs1  27463  mamuvs2  27464  mendrng  27500  idomrootle  27511  proot1mul  27515  proot1hash  27519  proot1ex  27520  deg1mhm  27526  fgraphopab  27529  hausgraph  27531  caofcan  27540  ofsubid  27541  ofmul12  27542  ofdivrec  27543  ofdivcan4  27544  ofdivdiv2  27545  expgrowthi  27550  dvconstbi  27551  expgrowth  27552  rfcnpre1  27690  rfcnpre2  27702  rfcnpre3  27704  rfcnpre4  27705  refsum2cnlem1  27708  climinf  27732  dvcosre  27741  stoweidlem20  27769  stoweidlem48  27797  fafvelrn  28032  ffnafv  28033  lfl1  29260  lfladdcl  29261  lflvscl  29267  ellkr  29279  lkr0f  29284  lkrsc  29287  eqlkr2  29290  eqlkr3  29291  ldualvaddval  29321  ldualvsval  29328  cdleme50rnlem  30733  tendoeq1  30953
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 5259
  Copyright terms: Public domain W3C validator