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

Theorem ffn 5558
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 5425 . 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 3288   ran crn 4846    Fn wfn 5416   -->wf 5417
This theorem is referenced by:  ffun  5560  frel  5561  fdm  5562  fresin  5579  fresaun  5581  fresaunres2  5582  fcoi1  5584  feu  5586  fnconstg  5598  f1fn  5607  fofn  5622  dffo2  5624  f1ofn  5642  feqmptd  5746  fvco3  5767  suppss  5830  suppssr  5831  ffvelrn  5835  dff2  5848  dffo3  5851  dffo4  5852  dffo5  5853  f1ompt  5858  ffnfv  5861  fcompt  5871  fsn2  5875  fconst2g  5913  fconstfv  5921  fex  5936  dff13  5971  cocan1  5991  soisores  6014  off  6287  ofco  6291  caofref  6297  caofid0l  6299  caofid0r  6300  caofid1  6301  caofid2  6302  caofrss  6304  caoftrn  6306  suppssof1  6313  fo1stres  6337  fo2ndres  6338  1stcof  6341  2ndcof  6342  curry1f  6407  curry2f  6409  fparlem1  6413  fparlem2  6414  fo2ndf  6420  fnwelem  6428  fnse  6430  tposf2  6470  smo11  6593  smorndom  6597  mapsn  7022  omxpenlem  7176  pw2f1olem  7179  mapen  7238  mapxpen  7240  mapunen  7243  f1finf1o  7302  unirnffid  7364  fissuni  7377  fipreima  7378  indexfi  7380  intrnfi  7387  marypha2  7410  ordtypelem7  7457  oismo  7473  wemapso2lem  7483  wemapso  7484  wemapso2  7485  unxpwdom2  7520  ixpiunwdom  7523  cantnfle  7590  cantnflt  7591  cantnfp1lem2  7599  cantnfp1lem3  7600  cantnfp1  7601  oemapvali  7604  cantnflem1a  7605  cantnflem1c  7607  cantnflem3  7611  cantnflem4  7612  cantnf  7613  mapfien  7617  cnfcomlem  7620  cnfcom3  7625  tcrank  7772  fseqenlem1  7869  numacn  7894  infpwfien  7907  carduniima  7941  cardinfima  7942  dfacacn  7985  cfflb  8103  cofsmo  8113  cfcoflem  8116  coftr  8117  fin23lem40  8195  isf32lem2  8198  isf34lem7  8223  isf34lem6  8224  axdc3lem2  8295  ac6num  8323  ac6c4  8325  ac6s2  8330  ttukeylem6  8358  iunfo  8378  unirnfdomd  8406  pwcfsdom  8422  fpwwe2lem6  8474  fpwwe2lem8  8476  pwfseqlem3  8499  inar1  8614  tskcard  8620  tskuni  8622  tskurn  8628  gruima  8641  nqerrel  8773  recmulnq  8805  dmrecnq  8809  axpre-sup  9008  ofsubeq0  9961  ofnegsub  9962  ofsubge0  9963  dfz2  10263  uzn0  10465  rpnnen1lem3  10566  rpnnen1lem5  10568  unirnioo  10968  dfioo2  10969  ioorebas  10970  fseq1p1m1  11085  injresinjlem  11162  fsequb2  11278  fseqsupcl  11279  fseqsupubi  11280  seqf1olem2  11326  ser0f  11339  hashgval  11584  hashinf  11586  hashgval2  11615  iswrd  11692  wrdf  11696  wrdfin  11697  ccatlid  11711  ccatrid  11712  ccatass  11713  eqs1  11724  swrd0len  11732  swrdid  11735  ccatswrd  11736  swrdccat1  11737  swrdccat2  11738  cats1un  11753  revlen  11757  revccat  11761  revrev  11762  lenco  11764  s1co  11765  revco  11766  ccatco  11767  shftf  11857  uzin2  12111  rexanuz  12112  limsupgle  12234  limsuple  12235  limsupval2  12237  rlimres  12315  lo1res  12316  rlimresb  12322  o1of2  12369  o1rlimmul  12375  isercolllem2  12422  isercolllem3  12423  isercoll  12424  isercoll2  12425  climsup  12426  fsumss  12482  supcvg  12598  eff2  12663  reeff1  12684  tanval  12692  ruclem4  12796  ruclem11  12802  ruclem12  12803  eucalg  13041  prmreclem6  13252  1arithlem4  13257  1arith  13258  vdwmc  13309  vdwlem1  13312  vdwlem2  13313  vdwlem6  13317  vdwlem8  13319  vdwlem9  13320  vdwlem12  13323  vdwlem13  13324  ramval  13339  0ram  13351  0ram2  13352  0ramcl  13354  ramub1lem1  13357  ramcl  13360  firest  13623  pwsle  13677  pwsleval  13678  pwsvscaval  13680  mrcuni  13809  mrcun  13810  invf1o  13957  funcres2c  14061  isfull2  14071  arwhoma  14163  setcmon  14205  setcepi  14206  uncfcurf  14299  yoniso  14345  isacs4lem  14557  acsmapd  14567  prdsplusgcl  14689  prdsidlem  14690  prdsmndd  14691  resmhm2b  14724  mhmima  14726  mhmeql  14727  prdspjmhm  14729  pwsco1mhm  14732  pwsco2mhm  14733  gsumval2a  14745  gsumval2  14746  gsumwmhm  14753  frmdss2  14771  isgrpinv  14818  grpinvf1o  14824  prdsinvlem  14889  cycsubgcl  14929  ghmrn  14982  ghmpreima  14990  ghmeql  14991  ghmnsgima  14992  ghmnsgpreima  14993  ghmeqker  14995  ghmf1o  14998  gass  15041  cntzmhm  15100  efginvrel2  15322  efgsfo  15334  efgredleme  15338  efgredlem  15342  efgcpbllemb  15350  frgpup3lem  15372  0frgp  15374  ghmplusg  15424  gexex  15431  torsubg  15432  prdscmnd  15439  gsumval3a  15475  gsumval3eu  15476  gsumval3  15477  gsumzres  15480  gsumzaddlem  15489  gsumzsplit  15492  gsumzoppg  15502  gsumpt  15508  prdsgsum  15515  dprdfcntz  15536  dprdfadd  15541  dprdfeq0  15543  dprdf11  15544  dprdlub  15547  dprdspan  15548  dprdf1o  15553  dprd2dlem1  15562  dprd2db  15564  dmdprdpr  15570  dprdpr  15571  dpjlem  15572  ablfac1eu  15594  pgpfaclem1  15602  prdsmulrcl  15680  prdsrngd  15681  prdscrngd  15682  prds1  15683  isabvd  15871  srngf1o  15905  prdsvscacl  16007  prdslmodd  16008  lmhmco  16082  lmhmplusg  16083  lmhmvsca  16084  lmhmf1o  16085  lmhmima  16086  lmhmpreima  16087  lmhmrnlss  16089  lmhmeql  16094  lspextmo  16095  psrbaglesupp  16396  psrbagcon  16399  psrbaglefi  16400  psrbagconf1o  16402  gsumbagdiaglem  16403  psrvscaval  16419  psrlidm  16430  psrridm  16431  psrass1  16432  psrdi  16433  psrdir  16434  mplsubglem  16461  mplvscaval  16474  subrgmvrf  16488  mplmonmul  16490  mplbas2  16494  mvrf2  16515  mplind  16525  psrplusgpropd  16592  coe1add  16620  coe1addfv  16621  coe1sclmulfv  16638  cnfldplusf  16691  cnfldsub  16692  chrrhm  16775  znunit  16807  pjfo  16905  lecldbas  17245  lmbr2  17285  cncnpi  17304  cncnp  17306  cnrest2  17312  cnpdis  17319  lmss  17324  lmff  17327  lmcnp  17330  pnrmopn  17369  cnt0  17372  cnt1  17376  cnhaus  17380  dnsconst  17404  rncmp  17421  cmpsub  17425  tgcmp  17426  hauscmplem  17431  concn  17450  2ndcctbss  17479  2ndcomap  17482  2ndcsep  17483  1stccnp  17486  kgenidm  17540  iskgen2  17541  1stckgenlem  17546  1stckgen  17547  kgen2cn  17552  ptpjpre1  17564  ptbasfi  17574  pttop  17575  ptopn  17576  ptuni  17587  ptval2  17594  tx1cn  17602  tx2cn  17603  ptpjcn  17604  ptpjopn  17605  ptclsg  17608  ptcnplem  17614  ptcnp  17615  upxp  17616  txcnmpt  17617  uptx  17618  txtube  17633  txcmplem1  17634  txcmplem2  17635  hauseqlcld  17639  txkgen  17645  xkohaus  17646  xkoptsub  17647  xkopt  17648  xkococnlem  17652  xkococn  17653  cnmpt11  17656  cnmpt21  17664  cnmpt22f  17668  cnmptcom  17671  qtopss  17708  qtopeu  17709  qtopomap  17711  qtopcmap  17712  kqffn  17718  hmeof1o2  17756  ptcmpfi  17806  xkocnv  17807  zfbas  17889  uzrest  17890  rnelfmlem  17945  rnelfm  17946  fmfnfmlem2  17948  fmfnfm  17951  lmflf  17998  alexsubALT  18043  ptcmplem1  18044  cnextfres  18060  tmdgsum  18086  clssubg  18099  ghmcnp  18105  tgphaus  18107  divstgplem  18111  prdstmdd  18114  prdstgpd  18115  tsmsres  18134  tsmsxplem1  18143  ucncn  18276  fmucnd  18283  psmetxrge0  18305  isxmet2d  18318  xmettpos  18340  prdsmet  18361  imasdsf1olem  18364  blrnps  18399  blrn  18400  blelrnps  18407  blelrn  18408  xmeterval  18423  xmetresbl  18428  tmslem  18473  tmsxms  18477  imasf1oxms  18480  comet  18504  stdbdxmet  18506  met2ndci  18513  prdsxmslem2  18520  prdsxms  18521  blval2  18566  metuel2  18570  isngp2  18605  isngp3  18606  tngngp2  18654  isnghm  18718  nmotri  18734  qtopbaslem  18753  qdensere  18765  cnbl0  18769  cnblcld  18770  cnfldms  18771  blssioo  18787  tgioo  18788  tgqioo  18792  xrtgioo  18798  xrsdsre  18802  xrge0tsms  18826  metdsre  18844  iimulcn  18924  bndth  18944  evth  18945  lebnumlem3  18949  nmhmcn  19089  cphsqrcl  19108  lmmbr2  19173  fmcfil  19186  caucfil  19197  causs  19212  lmcau  19226  bcthlem4  19241  bcth3  19245  cncms  19270  cnfldcusp  19272  ivthicc  19316  evthicc2  19318  ovolfioo  19325  ovolficc  19326  ovolficcss  19327  ovolfsf  19329  ovolmge0  19334  ovollb2lem  19345  ovolunlem1a  19353  ovoliunlem1  19359  ovoliunlem2  19360  ovoliun  19362  ovoliun2  19363  ovolshftlem1  19366  ovolscalem1  19370  ovolicc1  19373  ovolicc2lem4  19377  ovolicc2  19379  ismbl  19383  voliunlem1  19405  voliunlem2  19406  voliunlem3  19407  volsup  19411  ioombl1lem2  19414  ioombl1lem4  19416  ioorf  19426  ioorinv  19429  ioorcl  19430  uniiccdif  19431  uniioovol  19432  uniiccvol  19433  uniioombllem2  19436  uniioombllem3  19438  uniioombllem4  19439  uniioombllem6  19441  dyaddisj  19449  dyadmax  19451  dyadmbllem  19452  dyadmbl  19453  opnmbllem  19454  opnmblALT  19456  volsup2  19458  vitalilem4  19464  mbfdm  19481  mbfima  19485  mbfid  19489  ismbfd  19493  mbfeqalem  19495  mbfres2  19498  mbfmulc2lem  19500  mbfmax  19502  mbfposr  19505  mbfimaopnlem  19508  mbfaddlem  19513  mbfadd  19514  mbfsub  19515  mbfsup  19517  mbfinf  19518  mbflimsup  19519  0plef  19525  itg1val2  19537  itg1ge0  19539  i1f1lem  19542  itg11  19544  itg1addlem1  19545  i1faddlem  19546  i1fmullem  19547  i1fadd  19548  i1fmul  19549  itg1addlem4  19552  i1fmulclem  19555  i1fmulc  19556  itg1mulc  19557  i1fres  19558  i1fpos  19559  itg10a  19563  itg1ge0a  19564  itg1lea  19565  itg1le  19566  itg1climres  19567  mbfi1fseqlem3  19570  mbfi1fseqlem4  19571  mbfi1fseqlem5  19572  mbfi1flimlem  19575  mbfmullem2  19577  mbfmul  19579  xrge0f  19584  itg2ge0  19588  itg20  19590  itg2seq  19595  itg2lea  19597  itg2splitlem  19601  itg2split  19602  itg2monolem1  19603  itg2monolem2  19604  itg2monolem3  19605  itg2mono  19606  itg2i1fseqle  19607  itg2i1fseq  19608  itg2i1fseq2  19609  itg2addlem  19611  itg2gt0  19613  itg2cnlem1  19614  itg2cnlem2  19615  itg2cn  19616  itgitg1  19661  bddmulibl  19691  bddibl  19692  limciun  19742  dvres  19759  dvres3a  19762  dvidlem  19763  cpnres  19784  dvaddbr  19785  dvmulbr  19786  dvaddf  19789  dvcmulf  19792  dvfre  19798  dvrec  19802  dvmptres3  19803  dvcnvlem  19821  rolle  19835  dvlip2  19840  dveq0  19845  dv11cn  19846  dvgt0lem2  19848  dvivthlem2  19854  dvivth  19855  dvne0  19856  lhop1lem  19858  lhop1  19859  lhop2  19860  lhop  19861  ftc1cn  19888  evlslem3  19896  evlslem1  19897  evlseu  19898  evlsvar  19905  evl1addd  19915  evl1subd  19916  evl1muld  19917  mpfconst  19920  mpfproj  19921  mpfsubrg  19922  mpfind  19926  pf1const  19927  pf1id  19928  pf1subrg  19929  mpfpf1  19932  pf1mpf  19933  pf1ind  19936  tdeglem4  19944  mdegleb  19948  mdegldg  19950  mdegaddle  19958  deg1fvi  19969  uc1pmon1p  20035  ply1remlem  20046  ply1rem  20047  fta1glem1  20049  fta1glem2  20050  fta1g  20051  fta1blem  20052  ig1peu  20055  ig1pdvds  20060  plyco0  20072  plyeq0lem  20090  plyeq0  20091  plypf1  20092  plyaddlem1  20093  coeeulem  20104  dgrlem  20109  dgrub  20114  dgrlb  20116  coeaddlem  20128  coemulc  20134  dgradd2  20147  dgrcolem2  20153  ofmulrt  20160  plyreres  20161  plydivlem3  20173  plydivlem4  20174  plydiveu  20176  plyremlem  20182  plyrem  20183  fta1lem  20185  fta1  20186  vieta1lem1  20188  vieta1lem2  20189  vieta1  20190  plyexmo  20191  elaa  20194  elqaalem3  20199  aannenlem1  20206  aalioulem2  20211  ulmuni  20269  ulmdvlem1  20277  ulmdv  20280  mbfulm  20283  iblulm  20284  itgulm  20285  pserulm  20299  psercnlem2  20301  psercnlem1  20302  psercn  20303  abelth  20318  reeff1o  20324  pilem1  20328  recosf1o  20398  resinf1o  20399  efif1olem3  20407  efif1olem4  20408  efifo  20410  eff1olem  20411  ellogrn  20418  logcn  20499  dvloglem  20500  logf1o2  20502  efopnlem1  20508  efopnlem2  20509  efopn  20510  logtayl  20512  cxpcn3lem  20592  cxpcn3  20593  resqrcn  20594  asinneg  20687  areambl  20758  rlimcnp2  20766  jensen  20788  amgm  20790  emcllem7  20801  basellem3  20826  basellem4  20827  basellem7  20830  basellem9  20832  sqff1o  20926  dvdsmulf1o  20940  fsumdvdsmul  20941  dchrelbas2  20982  dchrmulcl  20994  dchrfi  21000  dchreq  21003  dchrresb  21004  dchrinv  21006  dchr1re  21008  sumdchr2  21015  dchr2sum  21018  lgsqrlem2  21087  lgsqrlem3  21088  rpvmasum2  21167  dchrisum0re  21168  ostthlem1  21282  ostth  21294  nbgraf1olem5  21416  is2wlk  21526  redwlklem  21566  fargshiftfv  21583  fargshiftf  21584  fargshiftf1  21585  fargshiftfo  21586  constr3pthlem3  21605  vdgr0  21632  eupacl  21652  eupapf  21655  eupaseg  21656  eupares  21658  eupath  21664  vdegp1ai  21667  vdegp1bi  21668  isgrpo2  21746  issubgoi  21859  ginvsn  21898  efghgrp  21922  vcoprnelem  22018  nvinvfval  22082  cnnvm  22135  sspg  22188  ssps  22190  sspmlem  22192  sspn  22196  nvo00  22223  nmlno0lem  22255  lnon0  22260  phoeqi  22320  ubthlem1  22333  hhip  22640  hhssabloi  22723  hhssnv  22725  hhsssh  22730  occllem  22766  shsel  22777  chscllem2  23101  pjfn  23172  df0op2  23216  hoeq  23224  hocofni  23231  hoaddfni  23234  hosubfni  23235  hon0  23257  ho01i  23292  hoeq1  23294  elnlfn  23392  kbpj  23420  nmlnop0iALT  23459  lnopco0i  23468  imaelshi  23522  nlelchi  23525  rnbra  23571  cnvbraval  23574  kbass2  23581  kbass5  23584  hmopidmchi  23615  hmopidmpji  23616  elpjrn  23654  ofrn2  24014  off2  24015  ofresid  24016  xppreima2  24021  feqmptdf  24036  fcomptf  24038  ofpreima  24042  hashresfn  24117  xrge0tsmsd  24184  kerunit  24222  kerf1hrm  24223  hauseqcn  24254  xpinpreima  24265  xpinpreima2  24266  tpr2rico  24271  mndpluscn  24273  rmulccn  24275  raddcn  24276  xrge0pluscn  24287  xrge0tmdOLD  24292  rge0scvg  24296  elzrhunit  24324  qqhval2lem  24326  qqhf  24331  qqhre  24347  indpi1  24380  indpreima  24383  esumcvg  24437  ofcf  24447  measfn  24519  meascnbl  24534  1stmbfm  24571  2ndmbfm  24572  mbfmcnt  24579  sibfof  24615  sitgclcn  24619  rrvfn  24664  lgamgulm2  24781  txsconlem  24888  iccllyscon  24898  rellyscon  24899  cvmseu  24924  cvmopnlem  24926  cvmliftmolem1  24929  cvmliftmolem2  24930  cvmliftlem6  24938  cvmliftlem7  24939  cvmliftlem8  24940  cvmliftlem9  24941  cvmliftlem10  24942  cvmliftlem11  24943  cvmliftlem15  24946  cvmlift2lem9a  24951  cvmlift2lem6  24956  cvmlift2lem7  24957  cvmlift2lem10  24960  cvmlift2lem12  24962  cvmliftphtlem  24965  cvmlift3lem8  24974  cvmlift3lem9  24975  ghomgrpilem2  25058  ghomfo  25063  prodf1f  25181  iprodefisumlem  25278  fprb  25351  soseq  25476  fullfunfnv  25707  fullfunfv  25708  eqeefv  25754  axlowdimlem6  25798  axlowdimlem8  25800  axlowdimlem9  25801  axlowdimlem11  25803  axlowdimlem12  25804  axlowdimlem14  25806  axlowdimlem17  25809  mblfinlem  26151  volsupnfl  26158  cnambfre  26162  itg2addnclem  26163  itg2addnclem2  26164  itg2addnclem3  26165  itg2addnc  26166  itg2gt0cn  26167  ftc1cnnc  26186  areacirc  26195  comppfsc  26285  tailfb  26304  filnetlem4  26308  indexdom  26334  sdclem2  26344  istotbnd3  26378  sstotbnd2  26381  sstotbnd  26382  isbndx  26389  isbnd3  26391  isbnd3b  26392  prdsbnd  26400  prdstotbnd  26401  ismtyhmeolem  26411  heibor1lem  26416  heiborlem1  26418  heibor  26428  rrnmet  26436  rrnequiv  26442  grpokerinj  26458  isdrngo2  26472  keridl  26540  ralxpmap  26640  lcomfsup  26645  elrfirn  26647  ismrcd1  26650  ismrcd2  26651  istopclsd  26652  isnacs2  26658  isnacs3  26662  nacsfix  26664  mapfzcons1  26671  mzpaddmpt  26696  mzpmulmpt  26697  mzpsubst  26703  mzpcompact2lem  26706  eq0rabdioph  26733  eldioph4b  26770  diophren  26772  mzpcong  26935  pw2f1ocnv  27006  pw2f1o2val2  27009  fnwe2lem2  27024  islmodfg  27043  kercvrlsm  27057  lmhmfgsplit  27060  pwssplit1  27064  pwssplit4  27067  dsmmbas2  27079  dsmm0cl  27082  dsmmacl  27083  dsmmsubg  27085  dsmmlss  27086  frlmbas  27099  frlmvscaval  27107  frlmsslss2  27121  frlmssuvc2  27123  frlmsslsp  27124  frlmlbs  27125  frlmup1  27126  frlmup2  27127  frlmup3  27128  frlmup4  27129  ellspd  27130  lindfmm  27173  lsslindf  27176  islindf4  27184  hbt  27210  dgrsub2  27215  mpaaeu  27231  rngunsnply  27254  f1omvdconj  27265  pmtrmvd  27274  pmtrfinv  27278  symgtrinv  27289  mamulid  27334  mamurid  27335  mamuass  27336  mamudi  27337  mamudir  27338  mamuvs1  27339  mamuvs2  27340  mendrng  27376  idomrootle  27387  proot1mul  27391  proot1hash  27395  proot1ex  27396  deg1mhm  27402  fgraphopab  27405  hausgraph  27407  caofcan  27416  ofsubid  27417  ofmul12  27418  ofdivrec  27419  ofdivcan4  27420  ofdivdiv2  27421  expgrowthi  27426  dvconstbi  27427  expgrowth  27428  rfcnpre1  27565  rfcnpre2  27577  cncmpmax  27578  rfcnpre3  27579  rfcnpre4  27580  refsum2cnlem1  27583  climinf  27607  dvcosre  27616  stoweidlem48  27672  fafvelrn  27909  ffnafv  27910  imarnf1pr  27973  hashfirdm  28004  hashfzdm  28005  frgrancvvdeqlemB  28149  lfl1  29565  lfladdcl  29566  lflvscl  29572  ellkr  29584  lkr0f  29589  lkrsc  29592  eqlkr2  29595  eqlkr3  29596  ldualvaddval  29626  ldualvsval  29633  cdleme50rnlem  31038  tendoeq1  31258
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