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

Theorem fndm 5588
Description: The domain of a function. (Contributed by NM, 2-Aug-1994.)
Assertion
Ref Expression
fndm  |-  ( F  Fn  A  ->  dom  F  =  A )

Proof of Theorem fndm
StepHypRef Expression
1 df-fn 5499 . 2  |-  ( F  Fn  A  <->  ( Fun  F  /\  dom  F  =  A ) )
21simprbi 462 1  |-  ( F  Fn  A  ->  dom  F  =  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1399   dom cdm 4913   Fun wfun 5490    Fn wfn 5491
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 185  df-an 369  df-fn 5499
This theorem is referenced by:  funfni  5589  fndmu  5590  fnbr  5591  fnco  5597  fnresdm  5598  fnresdisj  5599  fnssresb  5601  fn0  5608  fnimadisj  5609  fnimaeq0  5610  dmmpti  5618  fdm  5643  f1dm  5693  f1odm  5728  f1o00  5756  fvelimab  5830  fvun1  5845  eqfnfv2  5884  fndmdif  5893  fneqeql2  5898  elpreima  5909  fsn2  5973  fnprb  6032  fconst3  6036  fconst4  6037  fnfvima  6051  fnunirn  6066  dff13  6067  nvof1o  6087  f1eqcocnv  6105  oprssov  6343  offval  6446  ofrfval  6447  fnexALT  6665  dmmpt2  6769  dmmpt2ga  6771  curry1  6791  curry1val  6792  curry2  6794  curry2val  6796  fparlem3  6801  fparlem4  6802  fnwelem  6814  suppvalfn  6824  suppfnss  6843  fnsuppres  6845  tposfo2  6896  smodm2  6944  smoel2  6952  tfrlem5  6967  tfrlem8  6971  tfrlem9  6972  tfrlem9a  6973  tfrlem13  6977  tfr2  6985  tz7.44-2  6991  tz7.44-3  6992  rdgsuc  7008  rdglim  7010  frsucmptn  7022  tz7.48-2  7025  tz7.48-1  7026  tz7.48-3  7027  tz7.49  7028  brwitnlem  7075  om0x  7087  oaabs2  7212  omabs  7214  elpmi  7356  elmapex  7358  pmresg  7365  pmsspw  7372  ixpprc  7409  undifixp  7424  bren  7444  fndmeng  7511  wemapso  7891  ixpiunwdom  7932  inf0  7952  r1suc  8101  r1lim  8103  r1ord  8111  r1ord3  8113  jech9.3  8145  onwf  8161  ssrankr1  8166  r1val3  8169  r1pw  8176  rankuni  8194  rankr1b  8195  alephcard  8364  alephnbtwn  8365  alephgeom  8376  dfac3  8415  dfac12lem1  8436  dfac12lem2  8437  cda1dif  8469  cdacomen  8474  cdadom1  8479  cdainf  8485  pwcdadom  8509  ackbij2lem3  8534  cfsmolem  8563  alephsing  8569  fin23lem31  8636  itunisuc  8712  itunitc1  8713  ituniiun  8715  hsmexlem6  8724  zorn2lem4  8792  ttukeylem3  8804  alephadd  8865  alephreg  8870  pwcfsdom  8871  cfpwsdom  8872  r1limwun  9025  r1wunlim  9026  rankcf  9066  inatsk  9067  r1tskina  9071  grur1  9109  dmaddpi  9179  dmmulpi  9180  genpdm  9291  fsuppmapnn0fiublem  11999  fsuppmapnn0fiub  12000  hashkf  12309  hashfn  12346  shftfn  12908  rlimi2  13339  phimullem  14311  0rest  14837  restsspw  14839  firest  14840  prdsbas2  14876  prdsplusgval  14880  prdsmulrval  14882  prdsleval  14884  prdsdsval  14885  prdsvscaval  14886  imasleval  14948  xpsfrnel2  14972  homfeqbas  15102  cidpropd  15116  2oppchomf  15130  sscpwex  15221  sscfn1  15223  sscfn2  15224  ssclem  15225  isssc  15226  rescval2  15234  issubc2  15242  cofuval  15288  resfval2  15299  resf1st  15300  resf2nd  15301  funcres  15302  fucbas  15366  fuchom  15367  xpcbas  15564  xpchomfval  15565  xpccofval  15568  oppchofcl  15646  oyoncl  15656  gsumpropd2lem  16017  frmdss2  16148  gicer  16441  psgndmsubg  16644  psgneldm  16645  psgneldm2  16646  psgnval  16649  prdsmgp  17372  lspextmo  17815  psgnghm  18707  psgnghm2  18708  dsmmbas2  18859  dsmmfi  18860  dsmmelbas  18861  frlmsslsp  18916  islindf4  18958  ofco2  19038  cldrcl  19612  iscldtop  19682  neiss2  19688  restrcl  19744  restbas  19745  ssrest  19763  resstopn  19773  ptval  20156  txdis1cn  20221  qtopcld  20299  qtoprest  20303  kqsat  20317  kqdisj  20318  kqcldsat  20319  isr0  20323  kqnrmlem1  20329  kqnrmlem2  20330  hmphtop  20364  hmpher  20370  elfm3  20536  ustn0  20808  nghmfval  21314  isnghm  21315  ovolunlem1  21993  uniiccdif  22072  cpncn  22424  cpnres  22425  ulmf2  22864  tglngne  24057  uhgraun  24432  umgraf  24439  vdgrfval  25016  eupai  25088  eupap1  25097  ghabloOLD  25488  fcoinver  27593  ofpreima  27653  ofpreima2  27654  fnct  27685  ofcfval  28246  probfinmeasb  28551  coinflipspace  28602  cvmtop1  28894  cvmtop2  28895  dfrdg2  29393  wfrlem3  29510  wfrlem4  29511  wfrlem9  29516  wfrlem12  29519  frrlem3  29554  frrlem4  29555  frrlem5e  29560  frrlem11  29564  imageval  29733  bpolylem  29963  filnetlem4  30365  sdclem2  30401  prdstotbnd  30456  heibor1lem  30471  ismrc  30799  dnnumch3lem  31158  dnnumch3  31159  aomclem4  31169  aomclem6  31171  fnchoice  31571  fnresdmss  31610  icccncfext  31856  stoweidlem35  31983  stoweidlem59  32007  fnresfnco  32377  fnbrafvb  32405  uhgun  32698  fnxpdmdm  32774  plusfreseq  32778  bnj564  34148  bnj945  34179  bnj545  34300  bnj548  34302  bnj570  34310  bnj900  34334  bnj929  34341  bnj983  34356  bnj1018  34367  bnj1110  34385  bnj1121  34388  bnj1145  34396  bnj1245  34417  bnj1253  34420  bnj1286  34422  bnj1280  34423  bnj1296  34424  bnj1311  34427  bnj1442  34452  bnj1450  34453  bnj1498  34464  bnj1514  34466  bnj1501  34470  diadm  37175  dibdiadm  37295  dibdmN  37297  dicdmN  37324  dihdm  37409
  Copyright terms: Public domain W3C validator