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

Theorem ffn 5495
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 5362 . 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 3238   ran crn 4793    Fn wfn 5353   -->wf 5354
This theorem is referenced by:  ffun  5497  frel  5498  fdm  5499  fresin  5516  fresaun  5518  fresaunres2  5519  fcoi1  5521  feu  5523  fnconstg  5535  f1fn  5544  fofn  5559  dffo2  5561  f1ofn  5579  feqmptd  5682  fvco3  5703  suppss  5765  suppssr  5766  ffvelrn  5770  dff2  5783  dffo3  5786  dffo4  5787  dffo5  5788  f1ompt  5793  ffnfv  5796  fcompt  5805  fsn2  5809  fconst2g  5846  fconstfv  5854  fex  5869  dff13  5904  cocan1  5924  soisores  5947  off  6220  ofco  6224  caofref  6230  caofid0l  6232  caofid0r  6233  caofid1  6234  caofid2  6235  caofrss  6237  caoftrn  6239  suppssof1  6246  fo1stres  6270  fo2ndres  6271  1stcof  6274  2ndcof  6275  curry1f  6340  curry2f  6342  fparlem1  6346  fparlem2  6347  fnwelem  6358  fnse  6360  tposf2  6400  smo11  6523  smorndom  6527  mapsn  6952  omxpenlem  7106  pw2f1olem  7109  mapen  7168  mapxpen  7170  mapunen  7173  f1finf1o  7232  unirnffid  7294  fissuni  7307  fipreima  7308  indexfi  7310  intrnfi  7317  marypha2  7339  ordtypelem7  7386  oismo  7402  wemapso2lem  7412  wemapso  7413  wemapso2  7414  unxpwdom2  7449  ixpiunwdom  7452  cantnfle  7519  cantnflt  7520  cantnfp1lem2  7528  cantnfp1lem3  7529  cantnfp1  7530  oemapvali  7533  cantnflem1a  7534  cantnflem1c  7536  cantnflem3  7540  cantnflem4  7541  cantnf  7542  mapfien  7546  cnfcomlem  7549  cnfcom3  7554  tcrank  7701  fseqenlem1  7798  numacn  7823  infpwfien  7836  carduniima  7870  cardinfima  7871  dfacacn  7914  cfflb  8032  cofsmo  8042  cfcoflem  8045  coftr  8046  fin23lem40  8124  isf32lem2  8127  isf34lem7  8152  isf34lem6  8153  axdc3lem2  8224  ac6num  8253  ac6c4  8255  ac6s2  8260  ttukeylem6  8288  iunfo  8308  unirnfdomd  8336  pwcfsdom  8352  fpwwe2lem6  8404  fpwwe2lem8  8406  pwfseqlem3  8429  inar1  8544  tskcard  8550  tskuni  8552  tskurn  8558  gruima  8571  nqerrel  8703  recmulnq  8735  dmrecnq  8739  axpre-sup  8938  ofsubeq0  9890  ofnegsub  9891  ofsubge0  9892  dfz2  10192  uzn0  10394  rpnnen1lem3  10495  rpnnen1lem5  10497  unirnioo  10896  dfioo2  10897  ioorebas  10898  fseq1p1m1  11012  injresinjlem  11086  fsequb2  11202  fseqsupcl  11203  fseqsupubi  11204  seqf1olem2  11250  ser0f  11263  hashgval  11508  hashinf  11510  hashgval2  11539  iswrd  11616  wrdf  11620  wrdfin  11621  ccatlid  11635  ccatrid  11636  ccatass  11637  eqs1  11648  swrd0len  11656  swrdid  11659  ccatswrd  11660  swrdccat1  11661  swrdccat2  11662  cats1un  11677  revlen  11681  revccat  11685  revrev  11686  lenco  11688  s1co  11689  revco  11690  ccatco  11691  shftf  11781  uzin2  12035  rexanuz  12036  limsupgle  12158  limsuple  12159  limsupval2  12161  rlimres  12239  lo1res  12240  rlimresb  12246  o1of2  12293  o1rlimmul  12299  isercolllem2  12346  isercolllem3  12347  isercoll  12348  isercoll2  12349  climsup  12350  fsumss  12406  supcvg  12522  eff2  12587  reeff1  12608  tanval  12616  ruclem4  12720  ruclem11  12726  ruclem12  12727  eucalg  12965  prmreclem6  13176  1arithlem4  13181  1arith  13182  vdwmc  13233  vdwlem1  13236  vdwlem2  13237  vdwlem6  13241  vdwlem8  13243  vdwlem9  13244  vdwlem12  13247  vdwlem13  13248  ramval  13263  0ram  13275  0ram2  13276  0ramcl  13278  ramub1lem1  13281  ramcl  13284  firest  13547  pwsle  13601  pwsleval  13602  pwsvscaval  13604  mrcuni  13733  mrcun  13734  invf1o  13881  funcres2c  13985  isfull2  13995  arwhoma  14087  setcmon  14129  setcepi  14130  uncfcurf  14223  yoniso  14269  isacs4lem  14481  acsmapd  14491  prdsplusgcl  14613  prdsidlem  14614  prdsmndd  14615  resmhm2b  14648  mhmima  14650  mhmeql  14651  prdspjmhm  14653  pwsco1mhm  14656  pwsco2mhm  14657  gsumval2a  14669  gsumval2  14670  gsumwmhm  14677  frmdss2  14695  isgrpinv  14742  grpinvf1o  14748  prdsinvlem  14813  cycsubgcl  14853  ghmrn  14906  ghmpreima  14914  ghmeql  14915  ghmnsgima  14916  ghmnsgpreima  14917  ghmeqker  14919  ghmf1o  14922  gass  14965  cntzmhm  15024  efginvrel2  15246  efgsfo  15258  efgredleme  15262  efgredlem  15266  efgcpbllemb  15274  frgpup3lem  15296  0frgp  15298  ghmplusg  15348  gexex  15355  torsubg  15356  prdscmnd  15363  gsumval3a  15399  gsumval3eu  15400  gsumval3  15401  gsumzres  15404  gsumzaddlem  15413  gsumzsplit  15416  gsumzoppg  15426  gsumpt  15432  prdsgsum  15439  dprdfcntz  15460  dprdfadd  15465  dprdfeq0  15467  dprdf11  15468  dprdlub  15471  dprdspan  15472  dprdf1o  15477  dprd2dlem1  15486  dprd2db  15488  dmdprdpr  15494  dprdpr  15495  dpjlem  15496  ablfac1eu  15518  pgpfaclem1  15526  prdsmulrcl  15604  prdsrngd  15605  prdscrngd  15606  prds1  15607  isabvd  15795  srngf1o  15829  prdsvscacl  15935  prdslmodd  15936  lmhmco  16010  lmhmplusg  16011  lmhmvsca  16012  lmhmf1o  16013  lmhmima  16014  lmhmpreima  16015  lmhmrnlss  16017  lmhmeql  16022  lspextmo  16023  psrbaglesupp  16324  psrbagcon  16327  psrbaglefi  16328  psrbagconf1o  16330  gsumbagdiaglem  16331  psrvscaval  16347  psrlidm  16358  psrridm  16359  psrass1  16360  psrdi  16361  psrdir  16362  mplsubglem  16389  mplvscaval  16402  subrgmvrf  16416  mplmonmul  16418  mplbas2  16422  mvrf2  16443  mplind  16453  psrplusgpropd  16523  coe1add  16551  coe1addfv  16552  coe1sclmulfv  16569  cnfldplusf  16618  cnfldsub  16619  chrrhm  16702  znunit  16734  pjfo  16832  lecldbas  17166  lmbr2  17206  cncnpi  17224  cncnp  17226  cnrest2  17231  cnpdis  17238  lmss  17243  lmff  17246  lmcnp  17249  pnrmopn  17288  cnt0  17291  cnt1  17295  cnhaus  17299  dnsconst  17323  rncmp  17340  cmpsub  17344  tgcmp  17345  hauscmplem  17350  concn  17369  2ndcctbss  17398  2ndcomap  17401  2ndcsep  17402  1stccnp  17405  kgenidm  17459  iskgen2  17460  1stckgenlem  17465  1stckgen  17466  kgen2cn  17471  ptpjpre1  17483  ptbasfi  17493  pttop  17494  ptopn  17495  ptuni  17506  ptval2  17513  tx1cn  17520  tx2cn  17521  ptpjcn  17522  ptpjopn  17523  ptclsg  17526  ptcnplem  17532  ptcnp  17533  upxp  17534  txcnmpt  17535  uptx  17536  txtube  17551  txcmplem1  17552  txcmplem2  17553  hauseqlcld  17557  txkgen  17563  xkohaus  17564  xkoptsub  17565  xkopt  17566  xkococnlem  17570  xkococn  17571  cnmpt11  17574  cnmpt21  17582  cnmpt22f  17586  cnmptcom  17589  qtopss  17623  qtopeu  17624  qtopomap  17626  qtopcmap  17627  kqffn  17633  hmeof1o2  17671  ptcmpfi  17721  xkocnv  17722  zfbas  17804  uzrest  17805  rnelfmlem  17860  rnelfm  17861  fmfnfmlem2  17863  fmfnfm  17866  lmflf  17913  alexsubALT  17958  ptcmplem1  17959  tmdgsum  17991  clssubg  18004  ghmcnp  18010  tgphaus  18012  divstgplem  18016  prdstmdd  18019  prdstgpd  18020  tsmsres  18039  tsmsxplem1  18048  isxmet2d  18105  xmettpos  18126  prdsmet  18147  imasdsf1olem  18150  blrn  18175  blelrn  18180  xmeterval  18191  xmetresbl  18196  tmslem  18241  tmsxms  18245  imasf1oxms  18248  comet  18272  stdbdxmet  18274  met2ndci  18281  prdsxmslem2  18288  prdsxms  18289  isngp2  18332  isngp3  18333  tngngp2  18381  isnghm  18445  nmotri  18461  qtopbaslem  18480  qdensere  18492  cnbl0  18496  cnblcld  18497  cnfldms  18498  blssioo  18514  tgioo  18515  tgqioo  18519  xrtgioo  18525  xrsdsre  18529  xrge0tsms  18553  metdsre  18571  iimulcn  18651  bndth  18671  evth  18672  lebnumlem3  18676  nmhmcn  18816  cphsqrcl  18835  lmmbr2  18900  fmcfil  18913  caucfil  18924  causs  18939  lmcau  18953  bcthlem4  18964  bcth3  18968  cncms  18989  ivthicc  19033  evthicc2  19035  ovolfioo  19042  ovolficc  19043  ovolficcss  19044  ovolfsf  19046  ovolmge0  19051  ovollb2lem  19062  ovolunlem1a  19070  ovoliunlem1  19076  ovoliunlem2  19077  ovoliun  19079  ovoliun2  19080  ovolshftlem1  19083  ovolscalem1  19087  ovolicc1  19090  ovolicc2lem4  19094  ovolicc2  19096  ismbl  19100  voliunlem1  19122  voliunlem2  19123  voliunlem3  19124  volsup  19128  ioombl1lem2  19131  ioombl1lem4  19133  ioorf  19143  ioorinv  19146  ioorcl  19147  uniiccdif  19148  uniioovol  19149  uniiccvol  19150  uniioombllem2  19153  uniioombllem3  19155  uniioombllem4  19156  uniioombllem6  19158  dyaddisj  19166  dyadmax  19168  dyadmbllem  19169  dyadmbl  19170  opnmbllem  19171  opnmblALT  19173  volsup2  19175  vitalilem4  19181  mbfdm  19198  mbfima  19202  mbfid  19206  ismbfd  19210  mbfeqalem  19212  mbfres2  19215  mbfmulc2lem  19217  mbfmax  19219  mbfposr  19222  mbfimaopnlem  19225  mbfaddlem  19230  mbfadd  19231  mbfsub  19232  mbfsup  19234  mbfinf  19235  mbflimsup  19236  0plef  19242  itg1val2  19254  itg1ge0  19256  i1f1lem  19259  itg11  19261  itg1addlem1  19262  i1faddlem  19263  i1fmullem  19264  i1fadd  19265  i1fmul  19266  itg1addlem4  19269  i1fmulclem  19272  i1fmulc  19273  itg1mulc  19274  i1fres  19275  i1fpos  19276  itg10a  19280  itg1ge0a  19281  itg1lea  19282  itg1le  19283  itg1climres  19284  mbfi1fseqlem3  19287  mbfi1fseqlem4  19288  mbfi1fseqlem5  19289  mbfi1flimlem  19292  mbfmullem2  19294  mbfmul  19296  xrge0f  19301  itg2ge0  19305  itg20  19307  itg2seq  19312  itg2lea  19314  itg2splitlem  19318  itg2split  19319  itg2monolem1  19320  itg2monolem2  19321  itg2monolem3  19322  itg2mono  19323  itg2i1fseqle  19324  itg2i1fseq  19325  itg2i1fseq2  19326  itg2addlem  19328  itg2gt0  19330  itg2cnlem1  19331  itg2cnlem2  19332  itg2cn  19333  itgitg1  19378  bddmulibl  19408  bddibl  19409  limciun  19459  dvres  19476  dvres3a  19479  dvidlem  19480  cpnres  19501  dvaddbr  19502  dvmulbr  19503  dvaddf  19506  dvcmulf  19509  dvfre  19515  dvrec  19519  dvmptres3  19520  dvcnvlem  19538  rolle  19552  dvlip2  19557  dveq0  19562  dv11cn  19563  dvgt0lem2  19565  dvivthlem2  19571  dvivth  19572  dvne0  19573  lhop1lem  19575  lhop1  19576  lhop2  19577  lhop  19578  ftc1cn  19605  evlslem3  19613  evlslem1  19614  evlseu  19615  evlsvar  19622  evl1addd  19632  evl1subd  19633  evl1muld  19634  mpfconst  19637  mpfproj  19638  mpfsubrg  19639  mpfind  19643  pf1const  19644  pf1id  19645  pf1subrg  19646  mpfpf1  19649  pf1mpf  19650  pf1ind  19653  tdeglem4  19661  mdegleb  19665  mdegldg  19667  mdegaddle  19675  deg1fvi  19686  uc1pmon1p  19752  ply1remlem  19763  ply1rem  19764  fta1glem1  19766  fta1glem2  19767  fta1g  19768  fta1blem  19769  ig1peu  19772  ig1pdvds  19777  plyco0  19789  plyeq0lem  19807  plyeq0  19808  plypf1  19809  plyaddlem1  19810  coeeulem  19821  dgrlem  19826  dgrub  19831  dgrlb  19833  coeaddlem  19845  coemulc  19851  dgradd2  19864  dgrcolem2  19870  ofmulrt  19877  plyreres  19878  plydivlem3  19890  plydivlem4  19891  plydiveu  19893  plyremlem  19899  plyrem  19900  fta1lem  19902  fta1  19903  vieta1lem1  19905  vieta1lem2  19906  vieta1  19907  plyexmo  19908  elaa  19911  elqaalem3  19916  aannenlem1  19923  aalioulem2  19928  ulmuni  19986  ulmdvlem1  19994  ulmdv  19997  mbfulm  20000  iblulm  20001  itgulm  20002  pserulm  20016  psercnlem2  20018  psercnlem1  20019  psercn  20020  abelth  20035  reeff1o  20041  pilem1  20045  recosf1o  20115  resinf1o  20116  efif1olem3  20124  efif1olem4  20125  efifo  20127  eff1olem  20128  ellogrn  20135  logcn  20216  dvloglem  20217  logf1o2  20219  efopnlem1  20225  efopnlem2  20226  efopn  20227  logtayl  20229  cxpcn3lem  20309  cxpcn3  20310  resqrcn  20311  asinneg  20404  areambl  20475  rlimcnp2  20483  jensen  20505  amgm  20507  emcllem7  20518  basellem3  20543  basellem4  20544  basellem7  20547  basellem9  20549  sqff1o  20643  dvdsmulf1o  20657  fsumdvdsmul  20658  dchrelbas2  20699  dchrmulcl  20711  dchrfi  20717  dchreq  20720  dchrresb  20721  dchrinv  20723  dchr1re  20725  sumdchr2  20732  dchr2sum  20735  lgsqrlem2  20804  lgsqrlem3  20805  rpvmasum2  20884  dchrisum0re  20885  ostthlem1  20999  ostth  21011  isgrpo2  21175  issubgoi  21288  ginvsn  21327  efghgrp  21351  vcoprnelem  21447  nvinvfval  21511  cnnvm  21564  sspg  21617  ssps  21619  sspmlem  21621  sspn  21625  nvo00  21652  nmlno0lem  21684  lnon0  21689  phoeqi  21749  ubthlem1  21762  hhip  22069  hhssabloi  22152  hhssnv  22154  hhsssh  22159  occllem  22195  shsel  22206  chscllem2  22530  pjfn  22601  df0op2  22645  hoeq  22653  hocofni  22660  hoaddfni  22663  hosubfni  22664  hon0  22686  ho01i  22721  hoeq1  22723  elnlfn  22821  kbpj  22849  nmlnop0iALT  22888  lnopco0i  22897  imaelshi  22951  nlelchi  22954  rnbra  23000  cnvbraval  23003  kbass2  23010  kbass5  23013  hmopidmchi  23044  hmopidmpji  23045  elpjrn  23083  ofrn2  23456  off2  23457  xppreima2  23462  feqmptdf  23478  fcomptf  23480  hashresfn  23559  xrge0tsmsd  23614  kerunit  23626  kerf1hrm  23627  hauseqcn  23648  xpinpreima  23659  xpinpreima2  23660  tpr2rico  23665  mndpluscn  23667  rmulccn  23669  raddcn  23670  xrge0pluscn  23681  xrge0tmdALT  23686  rge0scvg  23690  ustuqtop  23749  fmucnd  23785  blval2  23807  cnfldcusp  23816  elzrhunit  23835  qqhval2lem  23837  qqhf  23842  qqhre  23852  indpi1  23884  indpreima  23887  esumcvg  23941  ofcf  23951  measfn  24022  meascnbl  24036  1stmbfm  24073  2ndmbfm  24074  mbfmcnt  24081  rrvfn  24151  coinflipspace  24186  lgamgulm2  24268  txsconlem  24374  iccllyscon  24384  rellyscon  24385  cvmseu  24410  cvmopnlem  24412  cvmliftmolem1  24415  cvmliftmolem2  24416  cvmliftlem6  24424  cvmliftlem7  24425  cvmliftlem8  24426  cvmliftlem9  24427  cvmliftlem10  24428  cvmliftlem11  24429  cvmliftlem15  24432  cvmlift2lem9a  24437  cvmlift2lem6  24442  cvmlift2lem7  24443  cvmlift2lem10  24446  cvmlift2lem12  24448  cvmliftphtlem  24451  cvmlift3lem8  24460  cvmlift3lem9  24461  eupacl  24471  eupapf  24474  eupaseg  24475  vdgr0  24479  eupares  24486  eupath  24492  vdegp1ai  24495  vdegp1bi  24496  ghomgrpilem2  24580  ghomfo  24585  prodf1f  24704  fprb  24870  soseq  24995  fullfunfnv  25226  fullfunfv  25227  eqeefv  25273  axlowdimlem6  25317  axlowdimlem8  25319  axlowdimlem9  25320  axlowdimlem11  25322  axlowdimlem12  25323  axlowdimlem14  25325  axlowdimlem17  25328  volsupnfl  25674  itg2addnclem  25675  itg2addnclem2  25676  itg2addnc  25677  itg2gt0cn  25678  ftc1cnnc  25697  areacirc  25706  comppfsc  25814  tailfb  25833  filnetlem4  25837  indexdom  25920  sdclem2  25959  istotbnd3  26001  sstotbnd2  26004  sstotbnd  26005  isbndx  26012  isbnd3  26014  isbnd3b  26015  prdsbnd  26023  prdstotbnd  26024  ismtyhmeolem  26034  heibor1lem  26039  heiborlem1  26041  heibor  26051  rrnmet  26059  rrnequiv  26065  grpokerinj  26081  isdrngo2  26095  keridl  26163  ralxpmap  26267  lcomfsup  26274  elrfirn  26276  ismrcd1  26279  ismrcd2  26280  istopclsd  26281  isnacs2  26287  isnacs3  26291  nacsfix  26293  mapfzcons1  26300  mzpaddmpt  26325  mzpmulmpt  26326  mzpsubst  26332  mzpcompact2lem  26335  eq0rabdioph  26362  eldioph4b  26400  diophren  26402  mzpcong  26565  pw2f1ocnv  26636  pw2f1o2val2  26639  fnwe2lem2  26654  islmodfg  26673  kercvrlsm  26687  lmhmfgsplit  26690  pwssplit1  26694  pwssplit4  26697  dsmmbas2  26709  dsmm0cl  26712  dsmmacl  26713  dsmmsubg  26715  dsmmlss  26716  frlmbas  26729  frlmvscaval  26737  frlmsslss2  26751  frlmssuvc2  26753  frlmsslsp  26754  frlmlbs  26755  frlmup1  26756  frlmup2  26757  frlmup3  26758  frlmup4  26759  ellspd  26760  lindfmm  26803  lsslindf  26806  islindf4  26814  hbt  26840  dgrsub2  26845  mpaaeu  26861  rngunsnply  26884  f1omvdconj  26895  pmtrmvd  26904  pmtrfinv  26908  symgtrinv  26919  mamulid  26964  mamurid  26965  mamuass  26966  mamudi  26967  mamudir  26968  mamuvs1  26969  mamuvs2  26970  mendrng  27006  idomrootle  27017  proot1mul  27021  proot1hash  27025  proot1ex  27026  deg1mhm  27032  fgraphopab  27035  hausgraph  27037  caofcan  27046  ofsubid  27047  ofmul12  27048  ofdivrec  27049  ofdivcan4  27050  ofdivdiv2  27051  expgrowthi  27056  dvconstbi  27057  expgrowth  27058  rfcnpre1  27196  rfcnpre2  27208  rfcnpre3  27210  rfcnpre4  27211  refsum2cnlem1  27214  climinf  27238  dvcosre  27247  stoweidlem20  27275  stoweidlem48  27303  fafvelrn  27541  ffnafv  27542  nbgraf1olem5  27611  redwlklem  27743  fargshiftfv  27760  fargshiftf  27761  fargshiftf1  27762  fargshiftfo  27763  constr3pthlem3  27783  vdgre0  27810  frgrancvvdeqlemB  27873  lfl1  29331  lfladdcl  29332  lflvscl  29338  ellkr  29350  lkr0f  29355  lkrsc  29358  eqlkr2  29361  eqlkr3  29362  ldualvaddval  29392  ldualvsval  29399  cdleme50rnlem  30804  tendoeq1  31024
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 5362
  Copyright terms: Public domain W3C validator