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

Theorem ffn 5550
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 5417 . 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 3280   ran crn 4838    Fn wfn 5408   -->wf 5409
This theorem is referenced by:  ffun  5552  frel  5553  fdm  5554  fresin  5571  fresaun  5573  fresaunres2  5574  fcoi1  5576  feu  5578  fnconstg  5590  f1fn  5599  fofn  5614  dffo2  5616  f1ofn  5634  feqmptd  5738  fvco3  5759  suppss  5822  suppssr  5823  ffvelrn  5827  dff2  5840  dffo3  5843  dffo4  5844  dffo5  5845  f1ompt  5850  ffnfv  5853  fcompt  5863  fsn2  5867  fconst2g  5905  fconstfv  5913  fex  5928  dff13  5963  cocan1  5983  soisores  6006  off  6279  ofco  6283  caofref  6289  caofid0l  6291  caofid0r  6292  caofid1  6293  caofid2  6294  caofrss  6296  caoftrn  6298  suppssof1  6305  fo1stres  6329  fo2ndres  6330  1stcof  6333  2ndcof  6334  curry1f  6399  curry2f  6401  fparlem1  6405  fparlem2  6406  fo2ndf  6412  fnwelem  6420  fnse  6422  tposf2  6462  smo11  6585  smorndom  6589  mapsn  7014  omxpenlem  7168  pw2f1olem  7171  mapen  7230  mapxpen  7232  mapunen  7235  f1finf1o  7294  unirnffid  7356  fissuni  7369  fipreima  7370  indexfi  7372  intrnfi  7379  marypha2  7402  ordtypelem7  7449  oismo  7465  wemapso2lem  7475  wemapso  7476  wemapso2  7477  unxpwdom2  7512  ixpiunwdom  7515  cantnfle  7582  cantnflt  7583  cantnfp1lem2  7591  cantnfp1lem3  7592  cantnfp1  7593  oemapvali  7596  cantnflem1a  7597  cantnflem1c  7599  cantnflem3  7603  cantnflem4  7604  cantnf  7605  mapfien  7609  cnfcomlem  7612  cnfcom3  7617  tcrank  7764  fseqenlem1  7861  numacn  7886  infpwfien  7899  carduniima  7933  cardinfima  7934  dfacacn  7977  cfflb  8095  cofsmo  8105  cfcoflem  8108  coftr  8109  fin23lem40  8187  isf32lem2  8190  isf34lem7  8215  isf34lem6  8216  axdc3lem2  8287  ac6num  8315  ac6c4  8317  ac6s2  8322  ttukeylem6  8350  iunfo  8370  unirnfdomd  8398  pwcfsdom  8414  fpwwe2lem6  8466  fpwwe2lem8  8468  pwfseqlem3  8491  inar1  8606  tskcard  8612  tskuni  8614  tskurn  8620  gruima  8633  nqerrel  8765  recmulnq  8797  dmrecnq  8801  axpre-sup  9000  ofsubeq0  9953  ofnegsub  9954  ofsubge0  9955  dfz2  10255  uzn0  10457  rpnnen1lem3  10558  rpnnen1lem5  10560  unirnioo  10960  dfioo2  10961  ioorebas  10962  fseq1p1m1  11077  injresinjlem  11154  fsequb2  11270  fseqsupcl  11271  fseqsupubi  11272  seqf1olem2  11318  ser0f  11331  hashgval  11576  hashinf  11578  hashgval2  11607  iswrd  11684  wrdf  11688  wrdfin  11689  ccatlid  11703  ccatrid  11704  ccatass  11705  eqs1  11716  swrd0len  11724  swrdid  11727  ccatswrd  11728  swrdccat1  11729  swrdccat2  11730  cats1un  11745  revlen  11749  revccat  11753  revrev  11754  lenco  11756  s1co  11757  revco  11758  ccatco  11759  shftf  11849  uzin2  12103  rexanuz  12104  limsupgle  12226  limsuple  12227  limsupval2  12229  rlimres  12307  lo1res  12308  rlimresb  12314  o1of2  12361  o1rlimmul  12367  isercolllem2  12414  isercolllem3  12415  isercoll  12416  isercoll2  12417  climsup  12418  fsumss  12474  supcvg  12590  eff2  12655  reeff1  12676  tanval  12684  ruclem4  12788  ruclem11  12794  ruclem12  12795  eucalg  13033  prmreclem6  13244  1arithlem4  13249  1arith  13250  vdwmc  13301  vdwlem1  13304  vdwlem2  13305  vdwlem6  13309  vdwlem8  13311  vdwlem9  13312  vdwlem12  13315  vdwlem13  13316  ramval  13331  0ram  13343  0ram2  13344  0ramcl  13346  ramub1lem1  13349  ramcl  13352  firest  13615  pwsle  13669  pwsleval  13670  pwsvscaval  13672  mrcuni  13801  mrcun  13802  invf1o  13949  funcres2c  14053  isfull2  14063  arwhoma  14155  setcmon  14197  setcepi  14198  uncfcurf  14291  yoniso  14337  isacs4lem  14549  acsmapd  14559  prdsplusgcl  14681  prdsidlem  14682  prdsmndd  14683  resmhm2b  14716  mhmima  14718  mhmeql  14719  prdspjmhm  14721  pwsco1mhm  14724  pwsco2mhm  14725  gsumval2a  14737  gsumval2  14738  gsumwmhm  14745  frmdss2  14763  isgrpinv  14810  grpinvf1o  14816  prdsinvlem  14881  cycsubgcl  14921  ghmrn  14974  ghmpreima  14982  ghmeql  14983  ghmnsgima  14984  ghmnsgpreima  14985  ghmeqker  14987  ghmf1o  14990  gass  15033  cntzmhm  15092  efginvrel2  15314  efgsfo  15326  efgredleme  15330  efgredlem  15334  efgcpbllemb  15342  frgpup3lem  15364  0frgp  15366  ghmplusg  15416  gexex  15423  torsubg  15424  prdscmnd  15431  gsumval3a  15467  gsumval3eu  15468  gsumval3  15469  gsumzres  15472  gsumzaddlem  15481  gsumzsplit  15484  gsumzoppg  15494  gsumpt  15500  prdsgsum  15507  dprdfcntz  15528  dprdfadd  15533  dprdfeq0  15535  dprdf11  15536  dprdlub  15539  dprdspan  15540  dprdf1o  15545  dprd2dlem1  15554  dprd2db  15556  dmdprdpr  15562  dprdpr  15563  dpjlem  15564  ablfac1eu  15586  pgpfaclem1  15594  prdsmulrcl  15672  prdsrngd  15673  prdscrngd  15674  prds1  15675  isabvd  15863  srngf1o  15897  prdsvscacl  15999  prdslmodd  16000  lmhmco  16074  lmhmplusg  16075  lmhmvsca  16076  lmhmf1o  16077  lmhmima  16078  lmhmpreima  16079  lmhmrnlss  16081  lmhmeql  16086  lspextmo  16087  psrbaglesupp  16388  psrbagcon  16391  psrbaglefi  16392  psrbagconf1o  16394  gsumbagdiaglem  16395  psrvscaval  16411  psrlidm  16422  psrridm  16423  psrass1  16424  psrdi  16425  psrdir  16426  mplsubglem  16453  mplvscaval  16466  subrgmvrf  16480  mplmonmul  16482  mplbas2  16486  mvrf2  16507  mplind  16517  psrplusgpropd  16584  coe1add  16612  coe1addfv  16613  coe1sclmulfv  16630  cnfldplusf  16683  cnfldsub  16684  chrrhm  16767  znunit  16799  pjfo  16897  lecldbas  17237  lmbr2  17277  cncnpi  17296  cncnp  17298  cnrest2  17304  cnpdis  17311  lmss  17316  lmff  17319  lmcnp  17322  pnrmopn  17361  cnt0  17364  cnt1  17368  cnhaus  17372  dnsconst  17396  rncmp  17413  cmpsub  17417  tgcmp  17418  hauscmplem  17423  concn  17442  2ndcctbss  17471  2ndcomap  17474  2ndcsep  17475  1stccnp  17478  kgenidm  17532  iskgen2  17533  1stckgenlem  17538  1stckgen  17539  kgen2cn  17544  ptpjpre1  17556  ptbasfi  17566  pttop  17567  ptopn  17568  ptuni  17579  ptval2  17586  tx1cn  17594  tx2cn  17595  ptpjcn  17596  ptpjopn  17597  ptclsg  17600  ptcnplem  17606  ptcnp  17607  upxp  17608  txcnmpt  17609  uptx  17610  txtube  17625  txcmplem1  17626  txcmplem2  17627  hauseqlcld  17631  txkgen  17637  xkohaus  17638  xkoptsub  17639  xkopt  17640  xkococnlem  17644  xkococn  17645  cnmpt11  17648  cnmpt21  17656  cnmpt22f  17660  cnmptcom  17663  qtopss  17700  qtopeu  17701  qtopomap  17703  qtopcmap  17704  kqffn  17710  hmeof1o2  17748  ptcmpfi  17798  xkocnv  17799  zfbas  17881  uzrest  17882  rnelfmlem  17937  rnelfm  17938  fmfnfmlem2  17940  fmfnfm  17943  lmflf  17990  alexsubALT  18035  ptcmplem1  18036  cnextfres  18052  tmdgsum  18078  clssubg  18091  ghmcnp  18097  tgphaus  18099  divstgplem  18103  prdstmdd  18106  prdstgpd  18107  tsmsres  18126  tsmsxplem1  18135  ucncn  18268  fmucnd  18275  psmetxrge0  18297  isxmet2d  18310  xmettpos  18332  prdsmet  18353  imasdsf1olem  18356  blrnps  18391  blrn  18392  blelrnps  18399  blelrn  18400  xmeterval  18415  xmetresbl  18420  tmslem  18465  tmsxms  18469  imasf1oxms  18472  comet  18496  stdbdxmet  18498  met2ndci  18505  prdsxmslem2  18512  prdsxms  18513  blval2  18558  metuel2  18562  isngp2  18597  isngp3  18598  tngngp2  18646  isnghm  18710  nmotri  18726  qtopbaslem  18745  qdensere  18757  cnbl0  18761  cnblcld  18762  cnfldms  18763  blssioo  18779  tgioo  18780  tgqioo  18784  xrtgioo  18790  xrsdsre  18794  xrge0tsms  18818  metdsre  18836  iimulcn  18916  bndth  18936  evth  18937  lebnumlem3  18941  nmhmcn  19081  cphsqrcl  19100  lmmbr2  19165  fmcfil  19178  caucfil  19189  causs  19204  lmcau  19218  bcthlem4  19233  bcth3  19237  cncms  19262  cnfldcusp  19264  ivthicc  19308  evthicc2  19310  ovolfioo  19317  ovolficc  19318  ovolficcss  19319  ovolfsf  19321  ovolmge0  19326  ovollb2lem  19337  ovolunlem1a  19345  ovoliunlem1  19351  ovoliunlem2  19352  ovoliun  19354  ovoliun2  19355  ovolshftlem1  19358  ovolscalem1  19362  ovolicc1  19365  ovolicc2lem4  19369  ovolicc2  19371  ismbl  19375  voliunlem1  19397  voliunlem2  19398  voliunlem3  19399  volsup  19403  ioombl1lem2  19406  ioombl1lem4  19408  ioorf  19418  ioorinv  19421  ioorcl  19422  uniiccdif  19423  uniioovol  19424  uniiccvol  19425  uniioombllem2  19428  uniioombllem3  19430  uniioombllem4  19431  uniioombllem6  19433  dyaddisj  19441  dyadmax  19443  dyadmbllem  19444  dyadmbl  19445  opnmbllem  19446  opnmblALT  19448  volsup2  19450  vitalilem4  19456  mbfdm  19473  mbfima  19477  mbfid  19481  ismbfd  19485  mbfeqalem  19487  mbfres2  19490  mbfmulc2lem  19492  mbfmax  19494  mbfposr  19497  mbfimaopnlem  19500  mbfaddlem  19505  mbfadd  19506  mbfsub  19507  mbfsup  19509  mbfinf  19510  mbflimsup  19511  0plef  19517  itg1val2  19529  itg1ge0  19531  i1f1lem  19534  itg11  19536  itg1addlem1  19537  i1faddlem  19538  i1fmullem  19539  i1fadd  19540  i1fmul  19541  itg1addlem4  19544  i1fmulclem  19547  i1fmulc  19548  itg1mulc  19549  i1fres  19550  i1fpos  19551  itg10a  19555  itg1ge0a  19556  itg1lea  19557  itg1le  19558  itg1climres  19559  mbfi1fseqlem3  19562  mbfi1fseqlem4  19563  mbfi1fseqlem5  19564  mbfi1flimlem  19567  mbfmullem2  19569  mbfmul  19571  xrge0f  19576  itg2ge0  19580  itg20  19582  itg2seq  19587  itg2lea  19589  itg2splitlem  19593  itg2split  19594  itg2monolem1  19595  itg2monolem2  19596  itg2monolem3  19597  itg2mono  19598  itg2i1fseqle  19599  itg2i1fseq  19600  itg2i1fseq2  19601  itg2addlem  19603  itg2gt0  19605  itg2cnlem1  19606  itg2cnlem2  19607  itg2cn  19608  itgitg1  19653  bddmulibl  19683  bddibl  19684  limciun  19734  dvres  19751  dvres3a  19754  dvidlem  19755  cpnres  19776  dvaddbr  19777  dvmulbr  19778  dvaddf  19781  dvcmulf  19784  dvfre  19790  dvrec  19794  dvmptres3  19795  dvcnvlem  19813  rolle  19827  dvlip2  19832  dveq0  19837  dv11cn  19838  dvgt0lem2  19840  dvivthlem2  19846  dvivth  19847  dvne0  19848  lhop1lem  19850  lhop1  19851  lhop2  19852  lhop  19853  ftc1cn  19880  evlslem3  19888  evlslem1  19889  evlseu  19890  evlsvar  19897  evl1addd  19907  evl1subd  19908  evl1muld  19909  mpfconst  19912  mpfproj  19913  mpfsubrg  19914  mpfind  19918  pf1const  19919  pf1id  19920  pf1subrg  19921  mpfpf1  19924  pf1mpf  19925  pf1ind  19928  tdeglem4  19936  mdegleb  19940  mdegldg  19942  mdegaddle  19950  deg1fvi  19961  uc1pmon1p  20027  ply1remlem  20038  ply1rem  20039  fta1glem1  20041  fta1glem2  20042  fta1g  20043  fta1blem  20044  ig1peu  20047  ig1pdvds  20052  plyco0  20064  plyeq0lem  20082  plyeq0  20083  plypf1  20084  plyaddlem1  20085  coeeulem  20096  dgrlem  20101  dgrub  20106  dgrlb  20108  coeaddlem  20120  coemulc  20126  dgradd2  20139  dgrcolem2  20145  ofmulrt  20152  plyreres  20153  plydivlem3  20165  plydivlem4  20166  plydiveu  20168  plyremlem  20174  plyrem  20175  fta1lem  20177  fta1  20178  vieta1lem1  20180  vieta1lem2  20181  vieta1  20182  plyexmo  20183  elaa  20186  elqaalem3  20191  aannenlem1  20198  aalioulem2  20203  ulmuni  20261  ulmdvlem1  20269  ulmdv  20272  mbfulm  20275  iblulm  20276  itgulm  20277  pserulm  20291  psercnlem2  20293  psercnlem1  20294  psercn  20295  abelth  20310  reeff1o  20316  pilem1  20320  recosf1o  20390  resinf1o  20391  efif1olem3  20399  efif1olem4  20400  efifo  20402  eff1olem  20403  ellogrn  20410  logcn  20491  dvloglem  20492  logf1o2  20494  efopnlem1  20500  efopnlem2  20501  efopn  20502  logtayl  20504  cxpcn3lem  20584  cxpcn3  20585  resqrcn  20586  asinneg  20679  areambl  20750  rlimcnp2  20758  jensen  20780  amgm  20782  emcllem7  20793  basellem3  20818  basellem4  20819  basellem7  20822  basellem9  20824  sqff1o  20918  dvdsmulf1o  20932  fsumdvdsmul  20933  dchrelbas2  20974  dchrmulcl  20986  dchrfi  20992  dchreq  20995  dchrresb  20996  dchrinv  20998  dchr1re  21000  sumdchr2  21007  dchr2sum  21010  lgsqrlem2  21079  lgsqrlem3  21080  rpvmasum2  21159  dchrisum0re  21160  ostthlem1  21274  ostth  21286  nbgraf1olem5  21408  is2wlk  21518  redwlklem  21558  fargshiftfv  21575  fargshiftf  21576  fargshiftf1  21577  fargshiftfo  21578  constr3pthlem3  21597  vdgr0  21624  eupacl  21644  eupapf  21647  eupaseg  21648  eupares  21650  eupath  21656  vdegp1ai  21659  vdegp1bi  21660  isgrpo2  21738  issubgoi  21851  ginvsn  21890  efghgrp  21914  vcoprnelem  22010  nvinvfval  22074  cnnvm  22127  sspg  22180  ssps  22182  sspmlem  22184  sspn  22188  nvo00  22215  nmlno0lem  22247  lnon0  22252  phoeqi  22312  ubthlem1  22325  hhip  22632  hhssabloi  22715  hhssnv  22717  hhsssh  22722  occllem  22758  shsel  22769  chscllem2  23093  pjfn  23164  df0op2  23208  hoeq  23216  hocofni  23223  hoaddfni  23226  hosubfni  23227  hon0  23249  ho01i  23284  hoeq1  23286  elnlfn  23384  kbpj  23412  nmlnop0iALT  23451  lnopco0i  23460  imaelshi  23514  nlelchi  23517  rnbra  23563  cnvbraval  23566  kbass2  23573  kbass5  23576  hmopidmchi  23607  hmopidmpji  23608  elpjrn  23646  ofrn2  24006  off2  24007  ofresid  24008  xppreima2  24013  feqmptdf  24028  fcomptf  24030  ofpreima  24034  hashresfn  24109  xrge0tsmsd  24176  kerunit  24214  kerf1hrm  24215  hauseqcn  24246  xpinpreima  24257  xpinpreima2  24258  tpr2rico  24263  mndpluscn  24265  rmulccn  24267  raddcn  24268  xrge0pluscn  24279  xrge0tmdOLD  24284  rge0scvg  24288  elzrhunit  24316  qqhval2lem  24318  qqhf  24323  qqhre  24339  indpi1  24372  indpreima  24375  esumcvg  24429  ofcf  24439  measfn  24511  meascnbl  24526  1stmbfm  24563  2ndmbfm  24564  mbfmcnt  24571  sibfof  24607  sitgclcn  24611  rrvfn  24656  lgamgulm2  24773  txsconlem  24880  iccllyscon  24890  rellyscon  24891  cvmseu  24916  cvmopnlem  24918  cvmliftmolem1  24921  cvmliftmolem2  24922  cvmliftlem6  24930  cvmliftlem7  24931  cvmliftlem8  24932  cvmliftlem9  24933  cvmliftlem10  24934  cvmliftlem11  24935  cvmliftlem15  24938  cvmlift2lem9a  24943  cvmlift2lem6  24948  cvmlift2lem7  24949  cvmlift2lem10  24952  cvmlift2lem12  24954  cvmliftphtlem  24957  cvmlift3lem8  24966  cvmlift3lem9  24967  ghomgrpilem2  25050  ghomfo  25055  prodf1f  25173  iprodefisumlem  25270  fprb  25343  soseq  25468  fullfunfnv  25699  fullfunfv  25700  eqeefv  25746  axlowdimlem6  25790  axlowdimlem8  25792  axlowdimlem9  25793  axlowdimlem11  25795  axlowdimlem12  25796  axlowdimlem14  25798  axlowdimlem17  25801  mblfinlem  26143  volsupnfl  26150  cnambfre  26154  itg2addnclem  26155  itg2addnclem2  26156  itg2addnclem3  26157  itg2addnc  26158  itg2gt0cn  26159  ftc1cnnc  26178  areacirc  26187  comppfsc  26277  tailfb  26296  filnetlem4  26300  indexdom  26326  sdclem2  26336  istotbnd3  26370  sstotbnd2  26373  sstotbnd  26374  isbndx  26381  isbnd3  26383  isbnd3b  26384  prdsbnd  26392  prdstotbnd  26393  ismtyhmeolem  26403  heibor1lem  26408  heiborlem1  26410  heibor  26420  rrnmet  26428  rrnequiv  26434  grpokerinj  26450  isdrngo2  26464  keridl  26532  ralxpmap  26632  lcomfsup  26637  elrfirn  26639  ismrcd1  26642  ismrcd2  26643  istopclsd  26644  isnacs2  26650  isnacs3  26654  nacsfix  26656  mapfzcons1  26663  mzpaddmpt  26688  mzpmulmpt  26689  mzpsubst  26695  mzpcompact2lem  26698  eq0rabdioph  26725  eldioph4b  26762  diophren  26764  mzpcong  26927  pw2f1ocnv  26998  pw2f1o2val2  27001  fnwe2lem2  27016  islmodfg  27035  kercvrlsm  27049  lmhmfgsplit  27052  pwssplit1  27056  pwssplit4  27059  dsmmbas2  27071  dsmm0cl  27074  dsmmacl  27075  dsmmsubg  27077  dsmmlss  27078  frlmbas  27091  frlmvscaval  27099  frlmsslss2  27113  frlmssuvc2  27115  frlmsslsp  27116  frlmlbs  27117  frlmup1  27118  frlmup2  27119  frlmup3  27120  frlmup4  27121  ellspd  27122  lindfmm  27165  lsslindf  27168  islindf4  27176  hbt  27202  dgrsub2  27207  mpaaeu  27223  rngunsnply  27246  f1omvdconj  27257  pmtrmvd  27266  pmtrfinv  27270  symgtrinv  27281  mamulid  27326  mamurid  27327  mamuass  27328  mamudi  27329  mamudir  27330  mamuvs1  27331  mamuvs2  27332  mendrng  27368  idomrootle  27379  proot1mul  27383  proot1hash  27387  proot1ex  27388  deg1mhm  27394  fgraphopab  27397  hausgraph  27399  caofcan  27408  ofsubid  27409  ofmul12  27410  ofdivrec  27411  ofdivcan4  27412  ofdivdiv2  27413  expgrowthi  27418  dvconstbi  27419  expgrowth  27420  rfcnpre1  27557  rfcnpre2  27569  cncmpmax  27570  rfcnpre3  27571  rfcnpre4  27572  refsum2cnlem1  27575  climinf  27599  dvcosre  27608  stoweidlem48  27664  fafvelrn  27901  ffnafv  27902  imarnf1pr  27965  hashfirdm  27996  hashfzdm  27997  frgrancvvdeqlemB  28141  lfl1  29553  lfladdcl  29554  lflvscl  29560  ellkr  29572  lkr0f  29577  lkrsc  29580  eqlkr2  29583  eqlkr3  29584  ldualvaddval  29614  ldualvsval  29621  cdleme50rnlem  31026  tendoeq1  31246
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 5417
  Copyright terms: Public domain W3C validator