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

Theorem ffn 6250
Description: A mapping is a function with domain. (Contributed by NM, 2-Aug-1994.)
Assertion
Ref Expression
ffn (𝐹:𝐴𝐵𝐹 Fn 𝐴)

Proof of Theorem ffn
StepHypRef Expression
1 df-f 6099 . 2 (𝐹:𝐴𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹𝐵))
21simplbi 487 1 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wss 3763  ran crn 5306   Fn wfn 6090  wf 6091
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 198  df-an 385  df-f 6099
This theorem is referenced by:  ffnd  6251  ffun  6253  frel  6255  fdm  6258  ffrn  6262  fresin  6282  fresaun  6284  fresaunres2  6285  fcoi1  6287  feu  6289  f0bi  6297  dffo2  6329  feqmptdf  6466  fvco3  6490  ffvelrn  6573  dff2  6587  dffo3  6590  dffo4  6591  dffo5  6592  f1ompt  6597  ffnfv  6604  frnssb  6607  fcompt  6617  fsn2  6620  fconst2g  6687  fpr2g  6694  fex  6708  dff13  6730  nvocnv  6755  soisores  6795  fo1stres  7418  fo2ndres  7419  1stcof  7422  2ndcof  7423  curry1f  7499  curry2f  7501  fparlem1  7505  fparlem2  7506  fo2ndf  7512  tposf2  7605  smo11  7691  mapsnd  8128  pw2f1olem  8297  mapen  8357  mapunen  8362  fissuni  8504  fipreima  8505  indexfi  8507  mapfien  8546  oismo  8678  cantnflt  8810  cantnfp1lem3  8818  cantnflem4  8830  tcrank  8988  updjudhcoinlf  9035  updjudhcoinrg  9036  updjud  9037  infpwfien  9162  carduniima  9196  cardinfima  9197  dfacacn  9242  cfflb  9360  cofsmo  9370  cfcoflem  9373  coftr  9374  fin23lem40  9452  axdc3lem2  9552  ac6num  9580  ac6c4  9582  ac6s2  9587  ttukeylem6  9615  iunfo  9640  pwcfsdom  9684  fpwwe2lem6  9736  fpwwe2lem8  9738  pwfseqlem3  9761  inar1  9876  tskcard  9882  tskuni  9884  tskurn  9890  gruima  9903  nqerrel  10033  recmulnq  10065  dmrecnq  10069  axpre-sup  10269  ofsubeq0  11296  dfz2  11655  uzn0  11914  rpnnen1lem3  12029  rpnnen1lem5  12031  unirnioo  12486  dfioo2  12487  ioorebas  12488  fseq1p1m1  12631  2ffzeq  12678  fvinim0ffz  12805  injresinjlem  12806  fsequb2  12993  fseqsupcl  12994  fseqsupubi  12995  ser0f  13071  hashgval  13334  hashinf  13336  hashresfn  13342  ffz0hash  13442  fnfzo0hash  13445  wrdred1hash  13556  ccatass  13579  ccatrn  13580  ccatswrd  13674  swrdccat1  13675  swrdccat2  13676  revlen  13729  revccat  13733  revrev  13734  repswlen  13741  repsdf2  13743  cshword  13755  0csh0  13757  lenco  13796  s1co  13797  cshco  13800  swrdco  13801  ofccat  13927  shftf  14036  uzin2  14301  rexanuz  14302  limsuple  14426  limsupval2  14428  rlimres  14506  lo1res  14507  rlimresb  14513  isercolllem2  14613  isercolllem3  14614  isercoll  14615  supcvg  14804  prodf1f  14839  eff2  15043  reeff1  15064  tanval  15072  ruclem4  15177  ruclem12  15184  prmreclem6  15836  1arithlem4  15841  1arith  15842  vdwmc  15893  vdwlem1  15896  vdwlem8  15903  vdwlem13  15908  ramval  15923  0ram  15935  0ram2  15936  0ramcl  15938  ramcl  15944  fsets  16096  firest  16292  0ssc  16695  0subcat  16696  isfull2  16769  arwhoma  16893  gsumval2a  17478  isgrpinv  17671  f1omvdconj  18061  pmtrmvd  18071  pmtrfinv  18076  pmtrdifellem4  18094  efginvrel2  18335  efgsfo  18347  efgredlem  18355  efgcpbllemb  18363  frgpup3lem  18385  0frgp  18387  gexex  18451  torsubg  18452  gsumval3  18503  gsumzres  18505  gsummptmhm  18535  gsumzoppg  18539  dprdf1o  18627  dprd2db  18638  pgpfaclem1  18676  kerf1hrm  18941  srngf1o  19052  lmhmima  19248  lmhmpreima  19249  lmhmrnlss  19251  lspextmo  19257  pwssplit1  19260  psrbaglefi  19575  psrlidm  19606  mplmonmul  19667  evlseu  19718  mpfconst  19732  mpfproj  19733  mpfsubrg  19734  coe1sclmulfv  19855  pf1const  19912  pf1id  19913  pf1subrg  19914  mpfpf1  19917  pf1mpf  19918  cnfldplusf  19975  cnfldsub  19976  chrrhm  20081  znunit  20113  psgnevpmb  20134  psgndiflemB  20148  mpt2frlmd  20320  frlmipval  20322  frlmphl  20324  frlmlbs  20340  frlmup4  20344  ellspd  20345  lindfmm  20370  lsslindf  20373  mamuass  20412  mamudi  20413  mamudir  20414  mamuvs1  20415  mamuvs2  20416  1mavmul  20559  mavmulass  20560  mdetunilem7  20629  madutpos  20653  lecldbas  21231  lmbr2  21271  cncnpi  21290  cncnp  21292  cnpdis  21305  lmff  21313  pnrmopn  21355  dnsconst  21390  cmpsub  21411  tgcmp  21412  hauscmplem  21417  2ndcctbss  21466  2ndcomap  21469  2ndcsep  21470  1stccnp  21473  kgenidm  21558  iskgen2  21559  1stckgen  21565  kgen2cn  21570  ptpjpre1  21582  pttop  21593  ptuni  21605  ptval2  21612  tx1cn  21620  tx2cn  21621  ptpjcn  21622  ptpjopn  21623  ptclsg  21626  ptcnplem  21632  upxp  21634  txcnmpt  21635  uptx  21636  txcmplem2  21653  txkgen  21663  xkoptsub  21665  xkopt  21666  xkococnlem  21670  xkococn  21671  ptcmpfi  21824  zfbas  21907  uzrest  21908  rnelfmlem  21963  rnelfm  21964  fmfnfmlem2  21966  fmfnfm  21969  lmflf  22016  alexsubALT  22062  clssubg  22119  qustgplem  22131  tsmsres  22154  tsmsxplem1  22163  ucncn  22296  xmettpos  22361  imasdsf1olem  22385  blrnps  22420  blrn  22421  xmeterval  22444  tmslem  22494  tmsxms  22498  imasf1oxms  22501  prdsxms  22542  blval2  22574  metuel2  22577  isngp2  22608  isngp3  22609  tngngp2  22663  isnghm  22734  qtopbaslem  22769  qdensere  22780  cnbl0  22784  cnblcld  22785  cnfldms  22786  blssioo  22805  tgioo  22806  tgqioo  22810  xrtgioo  22816  xrsdsre  22820  xrge0tsms  22844  iimulcn  22944  bndth  22964  lebnumlem3  22969  nmhmcn  23126  cphsqrtcl  23190  lmmbr2  23263  caucfil  23287  causs  23302  lmcau  23317  bcth3  23334  cncms  23357  cnfldcusp  23359  rrxmvallem  23393  ivthicc  23433  ovolfioo  23442  ovolficc  23443  ovolficcss  23444  ovollb2lem  23463  ovoliunlem2  23478  ovolshftlem1  23484  ovolicc2  23497  ismbl  23501  voliunlem2  23526  volsup  23531  ioorf  23548  ioorinv  23551  ioorcl  23552  uniiccdif  23553  uniioovol  23554  uniiccvol  23555  uniioombllem2  23558  uniioombllem4  23561  dyaddisj  23571  dyadmax  23573  dyadmbllem  23574  dyadmbl  23575  opnmbllem  23576  opnmblALT  23578  volsup2  23580  mbfdm  23601  mbfima  23605  mbfid  23610  ismbfd  23614  mbfres2  23620  mbfposr  23627  mbfimaopnlem  23630  mbflimsup  23641  0plef  23647  itg1val2  23659  i1f1lem  23664  itg11  23666  itg1addlem4  23674  i1fpos  23681  itg1le  23688  itg1climres  23689  mbfi1fseqlem5  23694  mbfi1flimlem  23697  xrge0f  23706  itg2ge0  23710  itg2seq  23717  itg2i1fseqle  23729  itg2i1fseq2  23731  itg2addlem  23733  itg2gt0  23735  limciun  23866  dvres  23883  dvres3a  23886  cpnres  23908  dvfre  23922  dvmptres3  23927  dvlip2  23966  dvgt0lem2  23974  deg1fvi  24053  uc1pmon1p  24119  fta1g  24135  ig1peu  24139  ig1pdvds  24144  plyco0  24156  plypf1  24176  dgrlem  24193  dgrub  24198  dgrlb  24200  coemulc  24219  plyreres  24246  plydivlem3  24258  plydivlem4  24259  plydiveu  24261  plyremlem  24267  fta1lem  24270  fta1  24271  vieta1lem2  24274  plyexmo  24276  elaa  24279  elqaalem3  24284  aannenlem1  24291  pserulm  24384  psercnlem2  24386  psercnlem1  24387  psercn  24388  abelth  24403  reeff1o  24409  pilem1  24413  recosf1o  24490  resinf1o  24491  efif1olem3  24499  efif1olem4  24500  efifo  24502  eff1olem  24503  ellogrn  24514  logcn  24601  dvloglem  24602  logf1o2  24604  efopnlem1  24610  efopnlem2  24611  efopn  24612  logtayl  24614  cxpcn3lem  24696  cxpcn3  24697  resqrtcn  24698  asinneg  24821  areambl  24893  emcllem7  24936  lgamgulm2  24970  basellem4  25018  sqff1o  25116  dvdsmulf1o  25128  fsumdvdsmul  25129  ostthlem1  25524  ostth  25536  tglnfn  25650  f1otrg  25959  axlowdimlem6  26035  axlowdimlem8  26037  axlowdimlem9  26038  axlowdimlem11  26040  axlowdimlem12  26041  axlowdimlem17  26046  crctcshlem4  26935  clwlkclwwlklem2  27137  clwlksfclwwlk1hashOLD  27228  clwlksf1clwwlklem1OLD  27233  eucrct2eupth  27412  cnnvm  27859  sspmlem  27909  nvo00  27938  nmlno0lem  27970  phoeqi  28035  ubthlem1  28048  hhip  28356  hhssabloilem  28440  hhssnv  28443  hhsssh  28448  occllem  28484  shsel  28495  chscllem2  28819  df0op2  28933  hoeq  28941  hocofni  28948  hoaddfni  28951  hosubfni  28952  hon0  28974  ho01i  29009  hoeq1  29011  elnlfn  29109  nmlnop0iALT  29176  lnopco0i  29185  imaelshi  29239  nlelchi  29242  rnbra  29288  cnvbraval  29291  kbass5  29301  hmopidmchi  29332  hmopidmpji  29333  foresf1o  29662  fimarab  29766  fcomptf  29779  ofpreima  29786  resf1o  29826  maprnin  29827  fpwrelmapffslem  29828  xrge0tsmsd  30104  kerunit  30142  txomap  30220  locfinreflem  30226  hauseqcn  30260  xpinpreima  30271  xpinpreima2  30272  tpr2rico  30277  mndpluscn  30291  rmulccn  30293  raddcn  30294  xrge0pluscn  30305  xrge0tmdOLD  30310  rge0scvg  30314  pl1cn  30320  elzrhunit  30342  qqhf  30349  cnrrext  30373  qqhre  30383  indpi1  30401  indpreima  30406  1stmbfm  30641  2ndmbfm  30642  mbfmcnt  30649  omssubadd  30681  carsggect  30699  eulerpartlemsv2  30739  eulerpartlems  30741  eulerpartlemv  30745  eulerpartlemb  30749  eulerpartlemf  30751  eulerpartlemt  30752  eulerpartlemmf  30756  eulerpartlemgvv  30757  eulerpartlemgh  30759  eulerpartlemgs2  30761  sseqmw  30772  sseqf  30773  sseqp1  30776  fiblem  30779  fibp1  30782  plymul02  30942  signsvtn0  30966  signstres  30971  signshlen  30986  reprinrn  31015  circlemethhgt  31040  txsconnlem  31539  iccllysconn  31549  rellysconn  31550  cvmseu  31575  cvmliftmolem2  31581  cvmliftlem6  31589  cvmliftlem7  31590  cvmliftlem8  31591  cvmliftlem9  31592  cvmliftlem11  31594  cvmliftlem15  31597  cvmlift2lem7  31608  cvmlift2lem10  31611  cvmlift3lem8  31625  cvmlift3lem9  31626  mvrsfpw  31720  mrsubff1  31728  msrid  31759  msrfo  31760  elmsta  31762  mtyf  31766  msubff1  31770  vhmcls  31780  mclsax  31783  elmthm  31790  mthmblem  31794  mclsppslem  31797  iprodefisumlem  31942  fprb  31985  soseq  32069  noetalem3  32180  madeval2  32251  fullfunfnv  32368  fullfunfv  32369  tailfb  32687  filnetlem4  32691  taupilem3  33476  icoreresf  33510  icoreelrnab  33512  relowlssretop  33521  relowlpssretop  33522  unccur  33699  matunitlindflem1  33712  matunitlindflem2  33713  ptrecube  33716  poimirlem28  33744  poimirlem32  33748  heicant  33751  opnmbllem0  33752  mblfinlem1  33753  mblfinlem2  33754  volsupnfl  33761  cnambfre  33764  dvtan  33766  itg2addnclem  33767  itg2addnclem2  33768  ftc1anclem3  33793  ftc1anclem5  33795  ftc1anclem7  33797  ftc1anclem8  33798  ftc1anc  33799  areacirc  33811  indexdom  33835  sdclem2  33843  sstotbnd2  33878  sstotbnd  33879  isbndx  33886  isbnd3b  33889  prdsbnd  33897  prdstotbnd  33898  ismtyhmeolem  33908  heibor1lem  33913  heiborlem1  33915  heibor  33925  rrnequiv  33939  keridl  34136  ellkr  34863  lkr0f  34868  cdleme50rnlem  36319  elrfirn  37754  ismrcd2  37758  isnacs2  37765  nacsfix  37771  mapfzcons1  37776  mzpcompact2lem  37810  eq0rabdioph  37836  eldioph4b  37871  diophren  37873  pw2f1ocnv  38099  pw2f1o2val2  38102  lmhmfgsplit  38151  pwssplit4  38154  hbt  38195  mpaaeu  38215  mendring  38257  proot1mul  38272  proot1hash  38273  proot1ex  38274  deg1mhm  38280  fgraphopab  38283  hausgraph  38285  ofsubid  39017  expgrowthi  39026  expgrowth  39028  binomcxplemdvbinom  39046  binomcxplemcvg  39047  binomcxplemnotnn0  39049  rfcnpre1  39666  rfcnpre2  39678  cncmpmax  39679  rfcnpre3  39680  rfcnpre4  39681  elixpconstg  39753  ffi  39837  dffo3f  39847  islptre  40325  resincncf  40562  dvcosre  40600  dvresntr  40606  volioof  40677  stoweidlem48  40738  fourierdlem12  40809  fourierdlem15  40812  fourierdlem41  40838  fourierdlem42  40839  fourierdlem46  40842  fourierdlem48  40844  fourierdlem49  40845  fourierdlem54  40850  fourierdlem56  40852  fourierdlem62  40858  fourierdlem64  40860  fourierdlem65  40861  fourierdlem73  40869  fourierdlem74  40870  fourierdlem75  40871  fourierdlem102  40898  fourierdlem103  40899  fourierdlem104  40900  fourierdlem114  40910  sge0split  41099  elhoi  41232  mbfresmf  41424  fafvelrn  41753  ffnafv  41754  fafv2elrn  41817  fafv2elrnb  41818  imarnf1pr  41866  2ffzoeq  41907  fargshiftfv  41944  fargshiftf  41945  fargshiftf1  41946  fargshiftfo  41947  ccatpfx  41978  cshword2  42006  zrinitorngc  42562  zrtermorngc  42563  zrtermoringc  42632  fdmdifeqresdif  42682  fdivmpt  42896  fdivmptf  42897  refdivmptf  42898  aacllem  43112
  Copyright terms: Public domain W3C validator